Jason Gross (Sep 11 2023 at 16:20): 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 <
shim doesn't work with native
Jason Gross (Sep 11 2023 at 16:22):Oh. How do I get native without installing?
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
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
Emilio Jesús Gallego Arias (Sep 11 2023 at 20:06):Yup this should be possible and of course desirable to solve !
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
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
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
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 topfor most devs
How does this interact with proof general, which, AIUI, expects a single executable for coqtop?
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.
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)
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.
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.
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: Nov 29 2023 at 22:01 UTC