How does one require proof-shell?

[proofgeneral]

How does one require proof-shell?

[cpitclaudel]

This was fixed a while ago

[Matafou]

Dunno.

Le mardi 24 novembre 2015, Clément Pit--Claudel [email protected]
a écrit :

I'm writing a plugin that depends on variables in proof-shell.el.
Unfortunately, requireing causes an error:

mapcar: Symbol’s value as variable is void: nil-completion-table

I found this bit in the source:

;; NB: completion table is expected to be set when proof-script;; is loaded! Call `proof-script-add-completions' to update.

(unless noninteractive ; during compilation
(eval-after-load "completion"
'(proof-add-completions)))

What’s the proper procedure?

—
Reply to this email directly or view it on GitHub
#14.

[DavidAspinall]

Some prover-specific variable names are generated from the proof
assistant name in a convoluted way. You probably want to do something
like this:

(require 'proof-site)
(proof-ready-for-assistant 'coq)
(require 'proof-shell)

• D.

On 24/11/2015 02:58, Clément Pit--Claudel wrote:

I'm writing a plugin that depends on variables in |proof-shell.el|.
Unfortunately, |require|ing causes an error:

|mapcar: Symbol’s value as variable is void: nil-completion-table|

I found this bit in the source:

;; NB: completion table is expected to be set when proof-script
;; is loaded! Call `proof-script-add-completions' to update.

(unless noninteractive; during compilation
(eval-after-load"completion"
'(proof-add-completions)))

What’s the proper procedure?

—
Reply to this email directly or view it on GitHub
#14.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[cpitclaudel]

Thanks David!

[cpitclaudel]

@DavidAspinall This only works partially, actually. My setup code is the following:

(require 'proof-site nil t)
(proof-ready-for-assistant 'coq) ;; Required by proof-shell
(require 'pg-vars)      ;; `proof-shell-proof-completed'
(require 'proof-config) ;; `proof-fly-past-comments'
(require 'proof-shell)  ;; `proof-shell-available-p'
(require 'coq-syntax)   ;; `coq-tactics-db'
(require 'coq)          ;; `coq-insert-match'

With this, the byte-compiler still complains:

company-coq.el:1368:36:Warning: reference to free variable
    ‘coq-hyp-name-in-goal-or-response-regexp’
company-coq.el:3590:1:Warning: the function ‘coq-insert-match’ is not known to
    be defined.

I tried adding an eval-and-compile around that block, but I get plenty of surprising errors:

Wrong type argument: keymapp, nil

[cpitclaudel]

@DavidAspinall Another issue with this is that it displays the splash screen, so users putting (require 'company-coq) in their.emacs` will always see the splash screen.

[DavidAspinall]

That sounds undesirable/wrong, I suspect some dependencies have been
broken somewhere. Can you run the autotest script "make test.coq"?
These tests used to work smoothly... - D.

On 07/01/2016 23:12, Clément Pit--Claudel wrote:

@DavidAspinall https://github.com/DavidAspinall Another issue with
this is that it displays the splash screen, so users putting |(require
'company-coq) in their|.emacs` will always see the splash screen.

—
Reply to this email directly or view it on GitHub
#14 (comment).

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[cpitclaudel]

Indeed, the tests fail: they open an Emacs window with the following message:

Welcome to  Proof General!
mapcar: Symbol’s value as variable is void: nil-completion-table