Stream: Coq devs & plugin devs

Topic: dev/shim/coqtop


view this post on Zulip Jason Gross (Sep 11 2023 at 16:20):

How about this one?

$ rlwrap dune exec -- dev/shim/coqtop
Welcome to Coq JasonGross-X1:/home/jgross/Documents/GitHub/coq/_build/default,more-float-tests (8ab822058e182da36e3b77a764cd5b38cb728ed6)

Eval native_compute in @id.
File "/tmp/Coq_native17c4aa/Coq_native7c5447.native", line 1, characters 5-17:
1 | open Nativevalues
         ^^^^^^^^^^^^
Error: Unbound module Nativevalues
Toplevel input, characters 0-27:
> Eval native_compute in @id.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Native compiler exited with status 2 (in case of stack overflow,
increasing stack size (typically with "ulimit -s") often helps)

Coq <

view this post on Zulip Gaëtan Gilbert (Sep 11 2023 at 16:21):

shim doesn't work with native

view this post on Zulip Jason Gross (Sep 11 2023 at 16:22):

Oh. How do I get native without installing?

view this post on Zulip Gaëtan Gilbert (Sep 11 2023 at 16:27):

I use dune exec -- coqtop (ie _build/install/default/bin/coqtop)
if you tried that you may have realized that this is problematic with native as native needs to be configured on, but it's hard to run configure in a way that the _build/install/bin/coqtop works (we should have a configure -local flag for this IMO but I got refused for reasons I couldn't understand last time I tried)

so what I do is I modify the configure call config/dune to add whatever arguments I want, then make world etc

view this post on Zulip Pierre-Marie Pédrot (Sep 11 2023 at 16:33):

Tangentially, this should be solved because this makes the life of native developers very annoying

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2023 at 20:06):

Yup this should be possible and of course desirable to solve !

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2023 at 20:07):

The shim can depend on the right files (like coq_config) and be rebuilt as needed

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2023 at 20:08):

We are at a point we could actually replace the shim by dune coq top for most devs

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2023 at 20:08):

but that's likely broken for the Coq bootstrap build in latest Dune versions

view this post on Zulip Jason Gross (Sep 12 2023 at 00:42):

Emilio Jesús Gallego Arias said:

We are at a point we could actually replace the shim by dune coq top for most devs

How does this interact with proof general, which, AIUI, expects a single executable for coqtop?

view this post on Zulip Paolo Giarrusso (Sep 12 2023 at 01:34):

Last I checked, dune coq top wasn't officially integrated in ProofGeneral, VsCoq 1, VsCoq 2, or Emilio's coq-lsp. I use a (slightly hacky) branch for VsCoq 1, I still needed to do one thing to merge it.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 12 2023 at 18:01):

I guess for PG would need dune as the command name and coq top as the first options ? coq-lsp / fcc are a bit different as they don't need Dune (they include a build system)

view this post on Zulip Paolo Giarrusso (Sep 12 2023 at 20:14):

IIRC from Abhishek's investigation, PG would try to pass _CoqProject options, and it does not pass a file name — there's no guarantee one exists, which makes perfect sense for coqtop and none for dune.

view this post on Zulip Paolo Giarrusso (Sep 12 2023 at 20:16):

If coq-lsp includes its own build system, I have to wonder how they'd invoke dune rules to generate (dependencies of) .v files.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 13 2023 at 08:52):

Paolo Giarrusso said:

If coq-lsp includes its own build system, I have to wonder how they'd invoke dune rules to generate (dependencies of) .v files.

That's not something supported yet, but in the future we will just call dune to build those.


Last updated: Jun 24 2024 at 13:02 UTC