Trying to support the rocq CLI.

[Matafou]

First attempt at supporting the new CLI: from coq v9, coq become rocq:

• coqtop becomes rocq top
• coqc become rocq c
• coqdep becomes rocq dep
• etc

@hendriktews can you have a look at what I did for compilation? I mainly reordered options to have the "dep" and "c" as the first option.

[Matafou]

@hendriktews please check in particular that this is still correct.

[Matafou]

@erikmd @hendriktews I don't know how to do that but we should add a new version of coq/rocq (V9) in the CI.

[erikmd]

Thanks @Matafou !!

Sorry, I have very little time this week :-/, but I'm willing to help if I can!

Meanwhile, FYI (Cc @hendriktews) I've just released the rocq/rocq-prover:9.0.0 image:

https://discourse.rocq-prover.org/t/docker-image-of-the-rocq-prover-rocq-rocq-prover-9-0/2545/2

[Chobbes]

I suspect this isn't ready to use just yet, and I'm just getting ahead of myself, but my attempts to pull this branch have resulted in the same issue as #811 where -emacs gets prepended to the arguments to rocq.

Happy to suffer and test this out, though, if that can be helpful :).

One concern that I had was for switching between projects (If I have a Coq 8.20 project / branch and a Rocq 9.0 project / branch)... But it seems like these changes support that, which is great!

[Chobbes]

@Matafou another problem I noticed --- I think currently there is no change to support _RocqProject yet.

[Matafou]

Thanks for testing @Chobbes ! From what you say I need to look at at least 2 things I didn't yet:

• the interaction with an already set proof-prog-args
• the project file (which I didn't even know about).
  About this last point, what is the recommended way when switching from v8 to v9? Have 2 files? One linking to the other? I wonder if I should just extend the regexp for detecting the project file or really deal with the possiblity that 2 files might co-exist.

[SkySkimmer]

Is anyone using _rocqproject?

[Matafou]

Is anyone using _rocqproject?

Not me. I guess the good practice must have exactly identical _coqProject and _rocqProject (wherever the capital letters should be :-))

[Chobbes]

Is anyone using _rocqproject?

I was trying to :).

Not me. I guess the good practice must have exactly identical _coqProject and _rocqProject (wherever the capital letters should be :-))

I have them linked right now to get around these issues.

About this last point, what is the recommended way when switching from v8 to v9? Have 2 files? One linking to the other? I wonder if I should just extend the regexp for detecting the project file or really deal with the possiblity that 2 files might co-exist.

I'm not sure what the intended transition is here. I am trying to build Vellvm with the new rocq makefile command (which replaces coq_makefile), and it works with a _RocqProject file. I'm actually not 100% sure if your patch to PG works with _RocqProject or not because of the argument order issues with rocq top. I did notice that my PG couldn't find stuff with coqtop 9.0 and a _RocqProject file, though, and grepping the PG project I find stuff about _CoqProject and nothing about _RocqProject --- but I'm not absolutely certain that this isn't something handled by rocq top over coqtop.

Happy to do what little I can to help with this, though! Feel free to ping me when there's a new patch and I'll happily test it out while working on Vellvm :)

[SkySkimmer]

Note that the name _CoqProject is just a convention as far as rocq makefile/coq_makefile are concerned, some projects name it eg Make instead. Or you can even invoke rocq makefile without a project file, eg rocq makefile -R . Foo bar.v -o Makefile.
Some editors (including PG) then recognize this name and get the configuration from it.

[Matafou]

True. It is hardwired in PG that it should be named _coqproject modulo capitals. This name is still recommended in Rocq documentation though.

[Matafou]

@Chobbes can you give more details about your project, or a link to an archive? I can't reproduce the misplaced "-emacs" option.

[Chobbes]

@Chobbes can you give more details about your project, or a link to an archive? I can't reproduce the misplaced "-emacs" option.

For sure. I'm working on porting Vellvm to 9.0 in this branch here https://github.com/vellvm/vellvm/tree/rocq-9.0 (I'm not 100% positive if the opam stuff there works because I'm in nix land and porting to Rocq 9.0 is a WIP)

If coqtop exists in the path the patched PG seems to work in that branch (e.g., trying to load the DynamicValues.v file), but if it's missing and I only have the rocq command I get a buffer containing this when I try to process the file:

Unknown subcommand -emacs
Usage: rocq [-debug-shim] {-v|--version|--print-version|--help|SUBCOMMAND} [ARGUMENTS...]

  -v, --version: print human readable version info
  --print-version: print machine readable version info

Supported subcommands:

    compile             Compile a Rocq source file
    c                   Alias for compile
    repl                Interactive read-eval-print loop
    top                 Alias for repl
    repl-with-drop      repl with Drop command
    top-with-drop       Alias for repl-with-drop
    native-precompile   Preprocess a compiled Rocq file for use by native_compute
    check               Check a compiled Rocq file (alias for command rocqchk)
    votour              Low level debugging of compiled files
    preprocess-mlg      Preprocess Rocq grammar files (.mlg) to produce OCaml sources
    pp-mlg              Alias for preprocess-mlg
    dep                 Print dependencies for compiling Rocq files
    doc                 Generate documentation from a Rocq source file
    wc                  Count lines of code in a Rocq source file
    workmgr             Control the number of parallel workers used by Rocq
    tex                 Process Rocq code in a Latex document
    makefile            Generate a Makefile to compile a Rocq project
    timelog2html        Combine timing information and a Rocq source file

Use "rocq subcommand --help" to get more information about a given subcommand.

It's possible I'm doing something wrong, I generally have PG installed via nix, so I'm loading the patched version manually with eval-buffer in the changed files... But I'm definitely getting the modified version, because otherwise it wouldn't try to call rocq at all!

I believe the relevant options in my emacs config for proof general are:

  (setq proof-splash-enable nil)
  (setq coq-compile-before-require t)
  (setq coq-compile-vos 'vos-and-vok)
  (setq coq-compile-quick 'no-quick)
  (setq proof-shell-kill-function-also-kills-associated-buffers t)
  (setq proof-multiple-frames-enable nil)

Hope that is vaguely helpful.

[Chobbes]

@Matafou if it's helpful, I'm happy to hop on a call at some point so I can show you directly what's going on for me, and maybe we can do a bit of debugging?

[Matafou]

When I start scripting in generic/proof-config.el I get this message:

Starting: "rocq" "top" "-emacs" "-topfile" "/home/courtieu/tmp/vellvm/src/rocq/Syntax/DynamicTypes.v" "-w" "-masking-absolute-name" "-w" "-deprecated-hint-without-locality" "-w" "-deprecated-hint-rewrite-without-locality" "-w" "-require-in-module" "-R" "/home/courtieu/tmp/vellvm/src/rocq" "Vellvm"

and it looks fine to me (although I didn't try to compile things to check further because you need extlib etc). So I guess your PG setting is maybe doing something wrong?

I will push a few more things tonight about the project file.

[Chobbes]

and it looks fine to me (although I didn't try to compile things to check further because you need extlib etc). So I guess your PG setting is maybe doing something wrong?

Hmmm, okay. Thank you for trying! I'll see if I can figure out what's going on later.

[SkySkimmer]

It seems that proof-prog-name-ask is not respected anymore? It still asks but my input is ignored and it just uses the program from PATH.

[Matafou]

Thanks for the input. I guess I have to be less aggressive in replacing prog-name.
For the moment I am struggling with the CI.

[Matafou]

• support proof-prog-name-ask (probably better interaction with auto compilation too)
• could not reproduce @Chobbes bug
• CI adapted to rocq cli and rocq prompts
• we should add rocq-9 in the CI
• A few people should test a bit more before merging.

[Chobbes]

@Matafou I pulled your latest changes and loaded them up in a fresh emacs with no config and it seems to work --- might have just been that I wasn't loading something properly 🤷, apologies for any confusion!

Thanks for getting this together, though :). It will be nice to have this working!

[Matafou]

OK thanks. So I guess I should adapt the options to the executable name (coqtop or rocq) instead of the version number? Don't really like this, but never mind.

[SkySkimmer]

Looking at the exe name is probably the easiest solution. You can also try to call $exe c with no other arguments, if it succeeds it's rocq otherwise it's coqtop

[monnier]

This seems wrong. We can look at the exe name (as done at line 131) or maybe the output of calling the exe with `-help`.

Or even `$coq-prog-name top </dev/null`?

[SkySkimmer]

That may work too

Although with top or c there are cases where it could fail even though with real arguments (particularly -coqlib) it would work

$coq-prog-name wc </dev/null may be more reliable

[Matafou]

Maybe the best thing to test is the rocq itself without any subcommand? Just testing its output.

[Matafou]

OK. Now I just call rocq and see if it outputs something containing "Supported subcommands:". Moreover I checked locally that CI tests do pass with rocq CLI.
I think it is time to merge and ask for wider testing volunteers. Will do in 2-3 days unless someone stops me.
Thanks all for your help!

[SkySkimmer]

Seems to work on my machine based tiny amount of testing

[Matafou]

FTR we should add some test involving proof-prog-name-ask. But for now it will do.

[erikmd]

BTW @Matafou it's ideal to be backed up up by CI's tests (especially for a key component like this),
and as said in #810 (comment), it'll be necessary to bump the PG/Emacs docker image for 9.0
so that it has rocq 9.0.0 and not the coq package,

but regarding the urgency to integrate the fix, I propose that we merge this as soon as you're happy with the PR,
and we'll be able to open another PR to add rocq 9.0.0 in CI tests (and last tweaks if need be)

WDYT? Cc @hendriktews

[SkySkimmer]

it'll be necessary to bump the PG/Emacs docker image for 9.0
so that it has rocq 9.0.0 and not the coq package,

you could also opam remove coq in your CI script

[Matafou]

Indeed the current #810 does not test the Rocq CLI. I did locally though.
OK let us merge this PR first then.
Will do on monday. And ask for testing on discourse maybe?

[erikmd]

you could also opam remove coq in your CI script

Yes but anyway, the image has to be updated, because it still refer to 9.0-rc1

[erikmd]

Will do on monday. And ask for testing on discourse maybe?

Good idea, thanks for proposing that!

[hendriktews]

Indeed the current #810 does not test the Rocq CLI.

I don't understand. Of course, #810 does not test any rocq commands, because it predates this PR. However, the rocq commands are present in the proofgeneral/coq-emacs:coq-9* images I prepared for #810.

#810 can be merged. I leave the decision on what to merge first to you.

[erikmd]

Hi!

@hendriktews Just to clarify what we meant with Pierre: the current 9.0 images that have been used to test PG in #810 did contain both rocq and coqtop binaries, cf. this comment.

As a result, if we merge both #815 and #810 (whatever is the merge order (but maybe it makes sense to put #810 first)), technically the CI won't test PG in a context where rocq is available and not coqtop. Because of the presence of the coq opam package in the current "9.0-rc1" image.

Hence the proposal to:

1. first merge (with a true merge) the PRs 810 then 815, in order not to delay the availability of rocq's CLI support,
2. then build new images for PG/rocq 9.0.0 (without coq)
3. and open another PR that uses them.

As noted by @SkySkimmer (as 2. 3. will take a bit of time), meanwhile it's possible to just add some opam remove -y coq coq-core in a relevant place in the GHA script… (opam remove coq wouldn't be enough.) WDYT?

[hendriktews]

#810 is merged now

[Matafou]

@hendriktews I realize that proof-tree MAY need some fix to work with rocq CLI.

[Matafou]

Or maybe not. Maybe proof-tree relies on the name of the default prompt being "Coq <"?

[Matafou]

Last question: owuld this be ok for now in CHANGES.md:

NOTE: for now the name of the rocq prover is still "Coq"
everywhere in PG. Renaming a prover in PG is not simple. It is not
clear yet when this will happen.

[erikmd]

Last question: owuld this be ok for now in CHANGES.md:

NOTE: for now the name of the rocq prover is still "Coq"
everywhere in PG. Renaming a prover in PG is not simple. It is not
clear yet when this will happen.

LGTM. Given PG should continue to support Coq <= 8.20 and Rocq >= 9.0 for a while, it looks irrelevant to also rename the features in PG. Also this would break company-coq and other Emacs distributions such as spacemacs and doom-emacs

[Matafou]

Renaming the prover is definitely complex in PG. Hundreds of variables are automatically named after the name of the prover...

[monnier]

Renaming the prover is definitely complex in PG. Hundreds of variables are automatically named after the name of the prover...

We should probably automatically give them both names (i.e. make one a `defvaralias` (or `define-obsolete-variable-alias`) of the other).

[Matafou]

Would that be possible without a huge refactoring?