Ana de Almeida Borges (Apr 27 2021 at 13:28): Ana de Almeida Borges (Apr 27 2021 at 13:28):Ok, I'm sure this is a silly question, but I'm guessing other people will run into it, so it's probably worth asking.
I was using make to build coq master, and now I'm trying to use dune. Here is what I did:
dune --version~/.config/dune/config with contents(lang dune 2.8)
(cache enabled)
make clean and git clean -dimake -f Makefile.dune worldThis resulted in many error messages similar to this one:
Error: Multiple rules generated for
_build/default/user-contrib/Ltac2/.Array.aux:
- file present in source tree
- <internal location>
Hint: rm -f user-contrib/Ltac2/.Array.aux
It's clear that deleting the .aux files would probably resolve this, but there are a lot of them. Is there a better way of removing them than rm with a regex?
Pierre-Marie Pédrot (Apr 27 2021 at 13:29):git clean -xdff is nuclear anihilation
Théo Zimmermann (Apr 27 2021 at 13:35):What does repeating f twice do?
Théo Zimmermann (Apr 27 2021 at 13:35):git clean dfx is indeed what I generally do, but when doing it you should probably verify with git status first that you don't have any untracked files that you may want to keep.
Pierre-Marie Pédrot (Apr 27 2021 at 13:36):Git will refuse to modify untracked nested git repositories (directories with a .git subdirectory) unless a second -f is given.
Ana de Almeida Borges (Apr 27 2021 at 13:39):One major consequence is that in principle, you should be able to switch between the dev modes of the two build systems (
./configure -profile devel && make -j4andmake -f Makefile.dune world) without having to call make clean or git clean anymore.
What is the difference between using these modes?
Ana de Almeida Borges (Apr 27 2021 at 13:47):What should I do to have coqtop back? Neither make nor make -f Makefile.dune world seem to have provided binaries (?)
Ana de Almeida Borges (Apr 27 2021 at 13:48):Is there a document I should be reading instead of asking these questions? https://github.com/coq/coq/blob/master/dev/doc/README.md seems to be outdated
Gaëtan Gilbert (Apr 27 2021 at 13:48):binaries are in _build/install/default/bin
Pierre-Marie Pédrot (Apr 27 2021 at 13:49):I have added these lines to my .bashrc:
export COQLIB=~/sources/coq/_build_vo/default/
export COQBIN=~/sources/coq/_build/install/default/bin/
(adapt to your system)
Ana de Almeida Borges (Apr 27 2021 at 14:17):I get a number of failures when running the test-suite. Many are related to ltac2:
Error:
File not found on loadpath : ltac2_plugin.cmxs
Also coq_makefile:
run.sh: line 5: coq_makefile: command not found
and some others.
Did I forget to compile something?
Pierre-Marie Pédrot (Apr 27 2021 at 14:18):I concur that I don't know how to build coq_makefile in the current setup
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:24):@Ana de Almeida Borges how are you calling the test suite?
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:26):@Pierre-Marie Pédrot , dune build _build/install/default/bin/coq_makefile`
Pierre-Marie Pédrot (Apr 27 2021 at 14:26):this would deserve an alias in the Makefile
Ana de Almeida Borges (Apr 27 2021 at 14:26):@Emilio Jesús Gallego Arias Yeah, I just realized I did make test-suite instead of make -f Makefile.dune test-suite. The latter works.
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:26):or if using make make _build/install/default/bin/coq_makefile
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:27):@Ana de Almeida Borges make test-suite should also work if you have done make world before
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:27):Pierre-Marie Pédrot said:
this would deserve an alias in the Makefile
Sure, tho if you are just calling it dune exec -- coq_makefile $args tends to be fine too
Ana de Almeida Borges (Apr 27 2021 at 14:27):I hadn't, I only did make and make -f Makefile.dune world
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:28):There are plans so you can do dune build %{bin:coq_makefile} etc... but I am not sure how many of these variables are implemented yet
Pierre-Marie Pédrot (Apr 27 2021 at 14:28):I can't mangle my binaries, this breaks all developments in the wild
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:28):what do you mean @Pierre-Marie Pédrot ?
Pierre-Marie Pédrot (Apr 27 2021 at 14:29):all scripts expect coq_makefile to be around
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:29):sure, I mean, how was around before?
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:30):before you had to add something to path
Pierre-Marie Pédrot (Apr 27 2021 at 14:30):I can't expect scripts to call dune exec -- blah
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:30):oh sure, I didn't mean that for script use
Pierre-Marie Pédrot (Apr 27 2021 at 14:30):most scripts expect the coq binaries to live in $COQBIN
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:31):then set COQBIN to _build/default/install/bin , and indeed execute the target you consider it proper
Gaëtan Gilbert (Apr 27 2021 at 14:31):the test-suite: world dep got removed?
Pierre-Marie Pédrot (Apr 27 2021 at 14:32):@Emilio Jesús Gallego Arias that's what I did indeed, but I have to invoke building these tools expliclty
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:32):Dune works a bit different here in that it doesn't require path mangling, if you declare the deps of your script things will be in scope
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:32):@Pierre-Marie Pédrot what target you used before?
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:33):to build a working set
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:33):@Gaëtan Gilbert it was not
Pierre-Marie Pédrot (Apr 27 2021 at 14:33):my magic command line: make -j -l4 bin/coqc pluginsbyte tools miniopt coqide states printers bin/coqc.byte bin/coqchk miniopt states bin/coqchk
Pierre-Marie Pédrot (Apr 27 2021 at 14:34):I guess there should be a tools target for the wrapper makefile
Pierre-Marie Pédrot (Apr 27 2021 at 14:34):hum, there is, but it doesn't compile coq_makefile
Ana de Almeida Borges (Apr 27 2021 at 14:38):Uh, I retract my "it works" from before. It works better... But now I have the following:
/bin/sh: 1: cannot create success/DHyp.v.log: Permission denied
DHyp.v seems to be an empty file. I'm very confused.
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:38):best approximation you can do now is make coq-core.install
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:39):@Ana de Almeida Borges this is due to leftovers in the build tree, there is an scenario that is not supported which is calling the test suite both from Makefile.make and Makefile.dune.
Ana de Almeida Borges (Apr 27 2021 at 14:40):Aha, this is exactly what I did. Can you explain or point to an explanation of what is the difference between using make and dune, and which I should be using?
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:41):For your use case, I would just set the COQ_USE_DUNE variable and use the targets there.
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:41):once you set that variable make will be make -f Makefile.dune
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:42):@Pierre-Marie Pédrot if the make coq-core.install is too slow for you we could have an alias for the byte stuff, however note that the overhead of compiling Init/Prelude.vo with coqc.byte is already greater than the native-code compilation in dev mode
Théo Zimmermann (Apr 27 2021 at 14:42):Ana de Almeida Borges said:
Is there a document I should be reading instead of asking these questions? https://github.com/coq/coq/blob/master/dev/doc/README.md seems to be outdated
I've opened https://github.com/coq/coq/pull/14184 to update it.
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:43):So if you are gonna compile a vo file I do recomment to use coqc not coqc.byte, unless you want to use the debugger tho [but in this case I'd use the debugger wrapper]
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:47):@Pierre-Marie Pédrot note that the tools target is still in the makefile , but likely not building the right set of things
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:47):Yup, for some reason it is not included in tools, bugfix upcoming.
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:51):Ups, that should be make _build/default/coq-core.install ; opam / dune where updated so now install files are out of tree too
Théo Zimmermann (Apr 27 2021 at 14:54):dune build coq-core.install should still work though?
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:56):Yup, as dune interprets targets under _build
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:56):but for make we need to refer to the real file
Emilio Jesús Gallego Arias (Apr 27 2021 at 14:57):unless we declare the target as phonhy
Emilio Jesús Gallego Arias (Apr 27 2021 at 15:02):ok, I confirm that the new layout in the "deprecate -local " PR was a good idea, and for example removes the need to have to set COQLIB to call binaries directly
Emilio Jesús Gallego Arias (Apr 27 2021 at 15:03):this is because if you call now binaries as _build_vo/default/bin/coqc , the auto-magic we have works
Emilio Jesús Gallego Arias (Apr 27 2021 at 15:13):By the way, regarding start up cost, the approach dune upstream is doing for 3.0 is to actually favor using dune as a demon with dune build --watch
Emilio Jesús Gallego Arias (Apr 27 2021 at 15:14):Testing on large codebases has helped fine-tune this mode, and it is always going to be much faster than calling dune build repeatedly, as it has to to build the DAG and check if all the deps have changed; however, when using -w, dune does use inotify or equivalent so it gets a very precise diff of the FS update.
Pierre-Marie Pédrot (Apr 27 2021 at 17:45):I am getting weird errors when trying to compile the ci targets locally.
Pierre-Marie Pédrot (Apr 27 2021 at 17:46):with make ci-mathcomp I get
make[1] : on entre dans le répertoire « /home/pm/sources/coq/_build_ci/mathcomp/mathcomp »
/home/pm/sources/coq/_build/install/default/bin/coq_makefile -f Make -o Makefile.coq
make[1]: *** [Makefile.common:55 : Makefile.coq] Erreur 1
make[1] : on quitte le répertoire « /home/pm/sources/coq/_build_ci/mathcomp/mathcomp »
make: *** [Makefile.ci:109 : ci-mathcomp] Erreur 2
this is after make world
Pierre-Marie Pédrot (Apr 27 2021 at 17:48):the same error occurs with most developments
Pierre-Marie Pédrot (Apr 27 2021 at 17:48):from what I gather, coq_makefile is not printing the right information to the output file which stays empty
Pierre-Marie Pédrot (Apr 27 2021 at 17:49):i.e. in this example _build_ci/mathcomp/mathcomp/Makefile.coq is empty when it should contain the autogenerated output
Pierre-Marie Pédrot (Apr 27 2021 at 17:51):I confirm that coq_makefile does not output anything when run
Pierre-Marie Pédrot (Apr 27 2021 at 17:52):without the -ooption it fails with Error: cannot find CoqMakefile.in
Pierre-Marie Pédrot (Apr 27 2021 at 17:54):looks like yet another issue with coqlib since coq_makefile looks for that file somewhere under coqlib / tools
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:19):Yup, this is due to that file not being found. How did you configure Coq? I'll try to repro
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:19):CI doesn't test all possible combinations, I tried to do my best
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:19):Upcoming PRs do clean up the code handling the location of stuff, making it canonical
Ana de Almeida Borges (Apr 27 2021 at 18:25):Pierre-Marie Pédrot said:
I have added these lines to my .bashrc:
export COQLIB=~/sources/coq/_build_vo/default/ export COQBIN=~/sources/coq/_build/install/default/bin/
Why do you map COQLIB to _build_vo and COQBIN to _build?
Ana de Almeida Borges (Apr 27 2021 at 18:30):Also, exporting these in .bashrc breaks coq when I change opam switches, which is not ideal. Do you have a workaround for it?
Emilio Jesús Gallego Arias (Apr 27 2021 at 18:34):@Ana de Almeida Borges I would not personally set that, indeed it is just a hack; if you use COQ_USE_DUNE, everything should work fine without hacks I think.
Ana de Almeida Borges (Apr 27 2021 at 18:36):Oh, you are right. Thanks!
Pierre-Marie Pédrot (Apr 28 2021 at 11:23):I am playing with the COQ_USE_DUNE setting, but it's even less functional than the hybrid make setting
Pierre-Marie Pédrot (Apr 28 2021 at 11:24):with make states, running coqc results in an error Error: Cannot find plugins directory
Pierre-Marie Pédrot (Apr 28 2021 at 11:24):and it doesn't solve https://github.com/coq/coq/issues/14187
Pierre-Marie Pédrot (Apr 28 2021 at 11:26):also, I still need to set COQLIB otherwise coqc won't find it
Pierre-Marie Pédrot (Apr 28 2021 at 11:26):what do?
Pierre-Marie Pédrot (Apr 28 2021 at 11:45):Ah, right, my COQLIB was pointing to the wrong place (the _build_vo folder for hybrid mode instead of _build)
Pierre-Marie Pédrot (Apr 28 2021 at 11:45):but I am still puzzled about what you said above @Emilio Jesús Gallego Arias
Pierre-Marie Pédrot (Apr 28 2021 at 11:46):you seemed to imply I wouldn't have to set COQLIB, which would be better because it's bad to have hidden bits of state lying around
Pierre-Marie Pédrot (Apr 28 2021 at 11:46):what setting do you recommend to make the binaries work?
Pierre-Marie Pédrot (Apr 28 2021 at 11:47):(I can't use dune exec -- blah because all the scripts in the wild expect my binaries to be the vanilla coqc / whatever)
Gaëtan Gilbert (Apr 28 2021 at 11:49):I just call the -prelude or install/ binaries directly
Pierre-Marie Pédrot (Apr 28 2021 at 11:49):wdym?
Pierre-Marie Pédrot (Apr 28 2021 at 11:49):as explained I have to set COQLIB otherwise it doesn't work
Enrico Tassi (Apr 28 2021 at 11:49):You are suggesting that -local is now replaced by make install?
Pierre-Marie Pédrot (Apr 28 2021 at 11:50):without COQLIB pointing to the _build/default directory I get
pm@ouranos:~/sources/coq$ /home/pm/sources/coq/_build/install/default/bin/coqc
Error:
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package contaning Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
ie instead of previously make states; bin/coqc bla I do dune build dev/shim/coqtop-prelude; _build/default/dev/shim/coqtop-prelude
Pierre-Marie Pédrot (Apr 28 2021 at 11:51):but how do you compile external devs?
Pierre-Marie Pédrot (Apr 28 2021 at 11:51):they expect coqc to be in the path
Gaëtan Gilbert (Apr 28 2021 at 11:53):the _build/install/default/bin/coqc also works for me, although I'm not sure what the minimal target for it is
Pierre-Marie Pédrot (Apr 28 2021 at 11:53):please help, I am getting a bit desperate
Pierre-Marie Pédrot (Apr 28 2021 at 11:53):even with a full world building I get the coqlib error
Gaëtan Gilbert (Apr 28 2021 at 11:54):what specific commands from git clean?
Gaëtan Gilbert (Apr 28 2021 at 11:55):also do you have any relevant variables set in your environment
Pierre-Marie Pédrot (Apr 28 2021 at 11:55):export COQ_USE_DUNE=1
make world
I've tried removing all the COQ* variables to no avail
Gaëtan Gilbert (Apr 28 2021 at 11:55):make world errors?
Pierre-Marie Pédrot (Apr 28 2021 at 11:55):no
Gaëtan Gilbert (Apr 28 2021 at 11:56):what errors then
Pierre-Marie Pédrot (Apr 28 2021 at 11:56):calling _build/install/default/bin/coqc
Gaëtan Gilbert (Apr 28 2021 at 11:56):specific command please
Pierre-Marie Pédrot (Apr 28 2021 at 11:56):this very command
Pierre-Marie Pédrot (Apr 28 2021 at 11:57):wait a sec
Pierre-Marie Pédrot (Apr 28 2021 at 11:57):I think I am messing up my environment variables
Pierre-Marie Pédrot (Apr 28 2021 at 11:58):let me start again from scratch
Pierre-Marie Pédrot (Apr 28 2021 at 11:59):in dune mode, from a clean state without crazy variables, make states is not enough for coqc to work
Pierre-Marie Pédrot (Apr 28 2021 at 12:00):pm@ouranos:~/sources/coq$ /home/pm/sources/coq/_build/install/default/bin/coqc
Error:
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package contaning Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
also dune exec -- dev/shim/coqtop-prelude does weird things
Gaëtan Gilbert (Apr 28 2021 at 12:02):https://github.com/coq/coq/blob/f4156a350f45e66c88c9cb2b12ce746e8aba3357/Makefile.dune#L17
Gaëtan Gilbert (Apr 28 2021 at 12:02):what meaning "weird things"
Pierre-Marie Pédrot (Apr 28 2021 at 12:02):CTRL-C, CTRL-D results in a not_found anomaly
Pierre-Marie Pédrot (Apr 28 2021 at 12:03):first time I ever saw that
Pierre-Marie Pédrot (Apr 28 2021 at 12:03):the backtrace tells me it's a parsing issue
Pierre-Marie Pédrot (Apr 28 2021 at 12:04):what should I understand from your link?
Pierre-Marie Pédrot (Apr 28 2021 at 12:04):coqtop doesn't work either
Gaëtan Gilbert (Apr 28 2021 at 12:04):your shell or terminal inserts a special character for ^C I guess
Pierre-Marie Pédrot (Apr 28 2021 at 12:04):pm@ouranos:~/sources/coq$ /home/pm/sources/coq/_build/install/default/bin/coqtop
Error:
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package contaning Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
(maybe for the shell, but it didn't do that before, I regularly CTRL-C CTRL-D to quit coqtop)
Gaëtan Gilbert (Apr 28 2021 at 12:04):the states target is specifically for the shim coqtop
Pierre-Marie Pédrot (Apr 28 2021 at 12:05):OK, but I don't want the shim
Pierre-Marie Pédrot (Apr 28 2021 at 12:05):I want my good old binary
Pierre-Marie Pédrot (Apr 28 2021 at 12:05):because the whole world expects this
Gaëtan Gilbert (Apr 28 2021 at 12:06):then tell dune to build the binary
Pierre-Marie Pédrot (Apr 28 2021 at 12:06):but the binary is here!
Gaëtan Gilbert (Apr 28 2021 at 12:06):right
Pierre-Marie Pédrot (Apr 28 2021 at 12:06):it's just not finding coqlib
Pierre-Marie Pédrot (Apr 28 2021 at 12:07):my workaround was to export COQLIB which actually works
Pierre-Marie Pédrot (Apr 28 2021 at 12:07):not that I really care, but I was promised a land of state-free environments
Gaëtan Gilbert (Apr 28 2021 at 12:07):please standby I'm looking at the anomaly
Pierre-Marie Pédrot (Apr 28 2021 at 12:08):(CTRL-C CTRL-D failing is not urgent, I can live with it)
Pierre-Marie Pédrot (Apr 28 2021 at 12:08):(my setup not working is slightly more urgent)
Gaëtan Gilbert (Apr 28 2021 at 12:12):dune build coq-core.install _build/install/default/lib/coq/theories/Init/Prelude.vo are enough for _build/install/default/bin/coqc for me
coq-core.install is somewhat more than needed but should be ok
Gaëtan Gilbert (Apr 28 2021 at 12:14):it wants the prelude file and something with plugins, not sure of the specifics for plugins
Pierre-Marie Pédrot (Apr 28 2021 at 12:14):can we get this added to the state target then?
Gaëtan Gilbert (Apr 28 2021 at 12:14):make a pr
Pierre-Marie Pédrot (Apr 28 2021 at 12:15):I have no idea which file should be modified
Pierre-Marie Pédrot (Apr 28 2021 at 12:15):whether Makefile.dune or the shim
Pierre-Marie Pédrot (Apr 28 2021 at 12:15):or something else
Gaëtan Gilbert (Apr 28 2021 at 12:15):Makefile.dune
Gaëtan Gilbert (Apr 28 2021 at 12:16):I can make the pr if you prefer
Pierre-Marie Pédrot (Apr 28 2021 at 12:16):wait a sec
Pierre-Marie Pédrot (Apr 28 2021 at 12:17):still doesn't work actually
Pierre-Marie Pédrot (Apr 28 2021 at 12:17):I get fancy errors when trying to compile external development with that
Pierre-Marie Pédrot (Apr 28 2021 at 12:17):(it magically solved the coq_makefile issue for some reason)
Pierre-Marie Pédrot (Apr 28 2021 at 12:18):Error: Cannot find library Coq.Init.Notations in loadpath
doesn't sound very good
Pierre-Marie Pédrot (Apr 28 2021 at 12:18):where is that hidden state again
Pierre-Marie Pédrot (Apr 28 2021 at 12:19):the miracle is that coqc works but not coqtop
Pierre-Marie Pédrot (Apr 28 2021 at 12:19):with your commands
pm@ouranos:~/sources/coq$ /home/pm/sources/coq/_build/install/default/bin/coqtop
Welcome to Coq 8.14+alpha
Error:
Cannot find library Coq.Init.Notations in loadpath (while searching for a .vos file)
coqc is silent in the same state
Pierre-Marie Pédrot (Apr 28 2021 at 12:21):(indeed if you pass it a file to compile it dies with the same error)
Gaëtan Gilbert (Apr 28 2021 at 12:22):x_x
Pierre-Marie Pédrot (Apr 28 2021 at 12:22):I think that the problem is not so much in the build
Pierre-Marie Pédrot (Apr 28 2021 at 12:23):rather, the loadpath initialization should handle this new situation
Pierre-Marie Pédrot (Apr 28 2021 at 12:23):because there are two places where the library might be found
Gaëtan Gilbert (Apr 28 2021 at 12:23):no, the problem is that dune is super annoying when you want minimal install targets
Pierre-Marie Pédrot (Apr 28 2021 at 12:23):_build/default/theories/ and _build/install/default/lib/coq/theories
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:23):Actually after the -local PR there will be a single place so hopefully all this works much better
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:23):you want to setup a minimal working env for applications
Gaëtan Gilbert (Apr 28 2021 at 12:24):you can do dune build coq-stdlib.install and interrupt once it starts talking about non Init vo files
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):for that you want , all in _build/install
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):and add that to the path
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):just dune build _build/install/default/lib/coq/theories/Init/Prelude.vo
Pierre-Marie Pédrot (Apr 28 2021 at 12:24):hm, but can't we have minimal install targets
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):yes you can
Pierre-Marie Pédrot (Apr 28 2021 at 12:24):I am not going to type that every 20s in my terminal
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):the thing is that states is only meant to be used from the shim
Pierre-Marie Pédrot (Apr 28 2021 at 12:25):states should build it for me
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):we can indeed reify it
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):adjust states so you get a install layout
Pierre-Marie Pédrot (Apr 28 2021 at 12:25):the coq_makefile issue seems very related
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):so indeed you want a target that setups coq_makefile + states
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):?
Pierre-Marie Pédrot (Apr 28 2021 at 12:25):coq_makefile should be set up by tools
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):I'd say don't pollute your env too much, just adjust path
Pierre-Marie Pédrot (Apr 28 2021 at 12:26):states should build me a functional coqc / coqtop
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:26):the thing is that tools may build the stuff
Pierre-Marie Pédrot (Apr 28 2021 at 12:26):(yeah, I tweak PATH depending on my needs)
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:26):but setting up the install layout is an extra step we may not be doing consistenly
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:26):and the code to locate stuff works over the install lyout
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:26):but that's not a biggy (even if annoying) adjusting some targets will do
Pierre-Marie Pédrot (Apr 28 2021 at 12:27):I am fine with partial install targets being run in my back
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:27):yes, actually very soon I hope we will have the coqlib locate code handle more cases
Pierre-Marie Pédrot (Apr 28 2021 at 12:27):the fact we are duplicating the build + install process looks like asking for trouble if you ask me
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:27):for example the library by Bobot in Dune to locate stuff works for both layouts
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:28):Pierre-Marie Pédrot said:
the fact we are duplicating the build + install process looks like asking for trouble if you ask me
What do you mean?
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:28):Where is the duplication?
Pierre-Marie Pédrot (Apr 28 2021 at 12:29):in the build and install directories, and that coqtop looks for both somewhat
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):coqtop is more dumb
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):install is just symlinks
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):actually you need something like install, as this is the stable layout on which clients of Coq can rely on
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):_build depends on how devs organize source code thus not stable
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):so there is not duplication per-se
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:31):just a rule that knows where to install things, which you ought to have anyways
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:31):so the trick is to understand that depending on things inside _build/default has a different layout, if you are building a rule for external programs to call coq, then you want for example to populate _build/install/default/bin to your needs
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):in fact dune does that automatically if you setup a rule
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):depending on coqc
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):for example, if you write (run coqc foo.v)
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):also @Pierre-Marie Pédrot an instructive command to understand what dune does to the build env is dune exec -- env
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):we will soon have dune shell which can drop you on a concrete env the rule is built on
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:34):So for example if you write:
(rule
(deps %{bin:coqc})
(run make mi-coq-dev))
the make scritpt will have coqc in path and ready; so indeed I didn't work too much on that use case of having a minimal setup, but it is a matter of adding the targets we want
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:35):I didn't work a lot on that because I prefer to work on porting stuff to dune, then I don't have to worry about any of this
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:35):as deps are tracked
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:36):But I think I understand what you need, basically a make target that builds an install a minimal setup up to a particular .vo file you pass to it from the stdlib
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:36):that should be easy
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:36):can you confirm @Pierre-Marie Pédrot ?
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:38):Regarding @Enrico Tassi question, -local is not replaced by make install, but by having a install tree in _build_vo
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:38):so just make produces the stuff in _build_vo or _build/install/$context
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:39):In Dune, make world will populate fully the install dir, so what we are missing is some smaller targets
Pierre-Marie Pédrot (Apr 28 2021 at 12:39):nah, in general I don't want a precise vo files
Pierre-Marie Pédrot (Apr 28 2021 at 12:39):most of the time, and this is what was done in the old makefile, I want to compile subfolders of theories/
Pierre-Marie Pédrot (Apr 28 2021 at 12:40):like fset, zarith and whatnot
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:42):Ok I will add an example for a set of .vo files, then we can add the needed aliases
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:43):I tend to single out a file
Pierre-Marie Pédrot (Apr 28 2021 at 12:44):it's too tiresome to have to write a single file, and most of the developments in the wild tend to require the meta-files
Pierre-Marie Pédrot (Apr 28 2021 at 12:45):can we get states to be fixed quickly?
Pierre-Marie Pédrot (Apr 28 2021 at 12:45):it's my basic tool in daily dev and it's quite cumbersome currently to have to spell out the full prelude file
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:47):use the shim as a workaround, I think I will have a PR fixing all your problems today
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:47):oh sorry, the shim won't work for you
Pierre-Marie Pédrot (Apr 28 2021 at 12:47):I can't use the shim because it won't work for external devs
Pierre-Marie Pédrot (Apr 28 2021 at 12:48):I believe I can survive for 24 to 48h without trying to touch external developments
Gaëtan Gilbert (Apr 28 2021 at 12:48):we could rename the shims to remove -prelude
Emilio Jesús Gallego Arias (Apr 28 2021 at 12:48):yup, use the workaround of having to use an alias to dune build _build/install/default/.../foo.vo until I submit the Pr
Pierre-Marie Pédrot (Apr 28 2021 at 12:49):@Emilio Jesús Gallego Arias this doesn't work for the prelude because it doesn't install all the files
Pierre-Marie Pédrot (Apr 28 2021 at 12:49):I'd need to explicitly list all the vo from the prelude
Gaëtan Gilbert (Apr 28 2021 at 12:50):tbh I'd like a dune command to say "put everything you can into install/ without building anything new"
Gaëtan Gilbert (Apr 28 2021 at 12:52):https://github.com/coq/coq/pull/14201
Pierre-Marie Pédrot (Apr 28 2021 at 12:53):isn't the reliance on the shell going to wreak havoc when passing quoted arguments?
Gaëtan Gilbert (Apr 28 2021 at 12:58):we can fix the quoting (added to pr)
Pierre-Marie Pédrot (Apr 28 2021 at 13:00):do I understand correctly this is a short-term solution?
Pierre-Marie Pédrot (Apr 28 2021 at 13:00):ideally I should just have to add the install binary folder to my PATH, right?
Pierre-Marie Pédrot (Apr 28 2021 at 13:00):not the shim one
Gaëtan Gilbert (Apr 28 2021 at 13:01):yes
I didn't actually test adding the shims to PATH so it might not even work tbh
Gaëtan Gilbert (Apr 28 2021 at 13:01):but the -prelude suffix is useless imo so we may as well remove it regardless
Emilio Jesús Gallego Arias (Apr 28 2021 at 13:02):@Pierre-Marie Pédrot indeed we will have to use a glob for now, tho for Dune 2.9 I have added "aliases" in the OCaml sense
Emilio Jesús Gallego Arias (Apr 28 2021 at 13:02):so you can refer to groups of files, for example you can do dune build theories/@vo-native to build all the native stuff only
Emilio Jesús Gallego Arias (Apr 28 2021 at 13:02):etc...
Emilio Jesús Gallego Arias (Apr 28 2021 at 13:02):let me work a bit on the POC to solve your immediate problem
Pierre-Marie Pédrot (Apr 28 2021 at 13:03):(also coq_makefile is not part of the shims, so this is not going to solve that problem)
Pierre-Marie Pédrot (Apr 29 2021 at 10:21):full dune build is not dying on coqc warnings, is that expected?
Pierre-Marie Pédrot (Apr 29 2021 at 10:23):(also the colouring of warning is not preserved by the dune compilation wrapper, I believe we should probably pass an explicit option to coqc)
Théo Zimmermann (Apr 29 2021 at 11:30):No, I think this is unexpected.
Pierre-Marie Pédrot (Apr 29 2021 at 11:49):the hybrid make does fail on warning, that said
Théo Zimmermann (Apr 29 2021 at 11:58):Sure, but this is completely independant.
Pierre-Marie Pédrot (Apr 29 2021 at 12:22):I am starting to be puzzled by the current situation. I must be doing something wrong because nothing works in the end, regardless of whether I use the pure dune or the hybrid setup. How do you people manage to use the dune + Coq build for development?
Pierre-Marie Pédrot (Apr 29 2021 at 12:22):Last woe is CoqIDE being unable to find the stdlib
Pierre-Marie Pédrot (Apr 29 2021 at 12:22):so I am trying to fix some files in the Coq stdlib and even with the shim, coqide doesn't know how to find the relevant vo files
Pierre-Marie Pédrot (Apr 29 2021 at 12:23):I must be missing something because this is literally one of the first thing you do when you write a patch.
Pierre-Marie Pédrot (Apr 29 2021 at 12:23):What do you people do?
Pierre-Marie Pédrot (Apr 29 2021 at 12:24):I can't make world or whatever because precisely it does not compile
Gaëtan Gilbert (Apr 29 2021 at 12:25):what did you try?
Pierre-Marie Pédrot (Apr 29 2021 at 12:25):(and I am not going to ask dune by hand to put the vo files in the install subdirectory)
Pierre-Marie Pédrot (Apr 29 2021 at 12:25):what should I try?
Pierre-Marie Pédrot (Apr 29 2021 at 12:25):make world fails
Pierre-Marie Pédrot (Apr 29 2021 at 12:25):I want to fix the stdlib, so I launch CoqIDE
Gaëtan Gilbert (Apr 29 2021 at 12:25):isn't it fine if make world fails? it's the same with the old system no, make would say
COQC la
COQC bli
error: bli failed
CoqIDE fails because the depending vo files are not in the path
Pierre-Marie Pédrot (Apr 29 2021 at 12:26):regardless of whether I use the shim or not
Pierre-Marie Pédrot (Apr 29 2021 at 12:26):what am I doing wrong?
Pierre-Marie Pédrot (Apr 29 2021 at 12:27):we don't have a target to ask for those vo files to be moved to install
Pierre-Marie Pédrot (Apr 29 2021 at 12:27):please help because in the last 48h or so my mental sanity has been taking a heavy toll
Gaëtan Gilbert (Apr 29 2021 at 12:28):I suppose in the old workflow you would do something like
edit something
make world # whatever fails
coqide whatever.v
now you do
edit something
make world
dune exec -- dev/shim/coqide-prelude whatever.v
(or _build/.../coqide-prelude if you know it's already built)
Pierre-Marie Pédrot (Apr 29 2021 at 12:28):but I can't edit
Pierre-Marie Pédrot (Apr 29 2021 at 12:28):coqide fails on Require
Pierre-Marie Pédrot (Apr 29 2021 at 12:28):because the vo files are not at the right place
Gaëtan Gilbert (Apr 29 2021 at 12:30):I literally just did
make -f Makefile.dune world (on clean state, succeeded)
remove the "Generalizable Variables" line in crelation classes
make -f Makefile.dune world (fails in crelationclasses)
dune exec -- dev/shim/coqide-prelude theories/Classes/CRelationClasses.v
it worked fine
Pierre-Marie Pédrot (Apr 29 2021 at 12:31):???
Pierre-Marie Pédrot (Apr 29 2021 at 12:31):did you run the file in CoqIDE?
Gaëtan Gilbert (Apr 29 2021 at 12:31):y
Pierre-Marie Pédrot (Apr 29 2021 at 12:31):it fails on Require
Gaëtan Gilbert (Apr 29 2021 at 12:31):n
Pierre-Marie Pédrot (Apr 29 2021 at 12:31):I did the very same thing.
Pierre-Marie Pédrot (Apr 29 2021 at 12:31):(Right now I am in hybrid mode but I have to keep switching because some stuff works in one mode but not in the other)
Pierre-Marie Pédrot (Apr 29 2021 at 12:32):let's try in pure dune mode
Gaëtan Gilbert (Apr 29 2021 at 12:34):btw how do you configure for hybrid mode? if you use -local you should check if https://github.com/coq/coq/pull/14176 still works for you
Pierre-Marie Pédrot (Apr 29 2021 at 12:35):I use -profile devel which probably sets local?
Gaëtan Gilbert (Apr 29 2021 at 12:36):y
Pierre-Marie Pédrot (Apr 29 2021 at 12:36):OK, so it works in pure dune mode
Pierre-Marie Pédrot (Apr 29 2021 at 12:37):(the problem with pure dune mode is that many useful targets are missing)
Gaëtan Gilbert (Apr 29 2021 at 12:37):the shims are only for pure dune mode to be clear
Pierre-Marie Pédrot (Apr 29 2021 at 12:37):right.
Pierre-Marie Pédrot (Apr 29 2021 at 12:37):so IIUC hybrid mode + local is broken
Pierre-Marie Pédrot (Apr 29 2021 at 12:38):because none of the tools are able to resolve COQLIB in a meaningful way
Pierre-Marie Pédrot (Apr 29 2021 at 12:45):(FTR I am having a lot of fun given that I am trying to fix warnings in the stdlib, which are non-fatal in dune mode, so I have to switch to hybrid mode, but then I can't edit files.)
Gaëtan Gilbert (Apr 29 2021 at 12:50):you can add -w +default to the flags in theories/dune
I don't know if it should always be enabled or conditionally somehow
Pierre-Marie Pédrot (Apr 29 2021 at 12:50):why don't we have a configure in dune mode? It's typically used for that
Gaëtan Gilbert (Apr 29 2021 at 12:50)::shrug:
Pierre-Marie Pédrot (Apr 29 2021 at 12:51):ok, no questions asked
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:01):we could make that a configure thing indeed and include the flags in the dune file
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:02):my workflow is like this @Pierre-Marie Pédrot
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:02):dune build theories/foo.vo
dune exec -- dev/shim/coq{c,ide} etc...
works pretty well, note that I don't set coqlib to the install path
Pierre-Marie Pédrot (Apr 29 2021 at 13:03):yes, I had intuited that messing with COQLIB was a bad idea
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):that is indeed not very well supported yet
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):as when I wanted to run ci-*
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):I do make world
Pierre-Marie Pédrot (Apr 29 2021 at 13:03):and how do you modify external developments?
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):so things work fine for my workflow
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):I just do make world, then for plugins, they are already dunerized
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):so just uncomment the (dirs ) line dune
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):and the make check
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):will include the plugins in ci-
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):for .v files, I am working on having all of ci dunerized too
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:05):so I don't have to care, I can just do dune build whatever.vo and I get a minimal rebuild
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:05):for now I have been relying on world
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:05):I but I have an approach where I never try to outdo the build system
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:06):I just use the few commands and if it is gonna take a minute I wait, but I play always on the safe side as having the typical interface mistach error is more painful for me
Pierre-Marie Pédrot (Apr 29 2021 at 13:07):I'll try to stay away from the hybrid mode, it seems to be broken for dev purposes
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:07):I'll make things much better once coq.boot goes in
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08):but indeed, there are very few reasons to use the hybrid mode when doing dev, native dune mode can do things like check very fast
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08):that's what I use all the time
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08):check
Pierre-Marie Pédrot (Apr 29 2021 at 13:08):if it is gonna take a minute I wait
not sure how beefy your machine is but typical build times are rather counted by chuks of 10 min
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08): Emilio Jesús Gallego Arias (Apr 29 2021 at 13:10):anything you are not happy with including slow build times open a bug, tho for you concrete problem of working with external devs the best solution is dunerize + cutoff , which is planned to happen soon
Pierre-Marie Pédrot (Apr 29 2021 at 13:11):I don't think you can solve slow Coq build times by tweaking the build system, but well
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:12):Oh we could improve a lot, if you look at trace file that dune generates
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:12):in my 4 core / 8 threads machine there is room for improvement
Pierre-Marie Pédrot (Apr 29 2021 at 13:12):I mean, I am talking about vo files that take > 10mn to compile
Pierre-Marie Pédrot (Apr 29 2021 at 13:12):contrarily to the typical OCaml file, Coq compilation is not IO-bound
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:12):Yup but when you have 8 cores, there is a lot of contention in our current build
Pierre-Marie Pédrot (Apr 29 2021 at 13:13):mathcomp is pretty terrible for instance
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:14):Indeed if you are gonna hack on math-comp you better get a beefy computer
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:15):but in terms of what make world takes, we got like a minute in my computer of margin to make it faster
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:15):there was a couple of terrible files
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:16):for now dune was optimized to hack on Coq + all the plugins simultaneously, now we got to optimize working with the things in ci a bit more indeed
Pierre-Marie Pédrot (Apr 29 2021 at 13:16):there is still coqdep taking ages on stdlib
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:17):That's fixed in 2.9 , 20 secs less
Pierre-Marie Pédrot (Apr 29 2021 at 13:17):I mean, not at boot, just when recompiling a file
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:17):Indeed I should have fixed that by now
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:17):yes I know, that was a bad design decision
Pierre-Marie Pédrot (Apr 29 2021 at 13:18):yes, I've seen some issue posted
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:18):We are releasing dune 2.9 as a maintenance release to fix that and to provide also full integration with devs in the ci in terms of general composition
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:22):cache does alleviate that to some extend
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:22):Please open the bug regading the make setup so I'm sure coq-boot does fix it
Pierre-Marie Pédrot (Apr 29 2021 at 13:24):if it's expected that the hybrid setup doesn't work with the shim, it's not a bug?
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:30):hybrid setup should work by calling the binaries directly
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:30):"as before"
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:31):After https://github.com/coq/coq/pull/14176 using _build_vo/default/bin/coqc for example
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:31):bin directory is used so we could indeed have it created as a symlink
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:31):is not used now I mean
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:32):indeed the shims will set coqlib to where the object files for the regular dune build work
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:32):we could have them test if _build_vo exists and then use that, I dunno
Pierre-Marie Pédrot (Apr 29 2021 at 13:33):but then I think it's just the same bug as before, i.e. COQLIB is wrong
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:33):yup that's a bug that's why we need the PR
Pierre-Marie Pédrot (Apr 29 2021 at 13:33):I mean that there is no point in opening an issue, we already have one opened for that
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:34):well in my testing the binaries were finding coqlib, but indeed there are couple of cases where it doesn't work
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:34):there are separate issues I think, but indeed, no need open if you want the problem is known
Pierre-Marie Pédrot (Apr 29 2021 at 13:35):I will wait for the dust to settle a bit and open issues if the problems persist despite the relevant PRs being merged
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:35):but assume $bin points to the directory where binaries are, then make states && $bin/coqc should work like before
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:35):if it doesn't it is a bug
Emilio Jesús Gallego Arias (Apr 29 2021 at 13:36):actually I will have bin be created as a synlink, that seems more user friendly, but the logic for coqlib location is pretty hairy in terms of symlinks etc...
Pierre-Marie Pédrot (Apr 29 2021 at 13:36):hm, I am a bit confused now
Pierre-Marie Pédrot (Apr 29 2021 at 13:37):As a dev I shouldn't use the hybrid mode
Pierre-Marie Pédrot (Apr 29 2021 at 13:37):so I am not sure of the usefulness of supporting this kind of dev setup
Pierre Roux (Apr 29 2021 at 14:17):When I call make -f Makefile.dune install, I'm asked to run dune install -p coq-core which gives
Error: The following <package>.install are missing:
- _build/default/coq-doc.install
- _build/default/coq-stdlib.install
- _build/default/coqide.install
- _build/default/coqide-server.install
Hint: try running: dune build @install
so I run dune build -p coq-stdlib @install and get
File "user-contrib/Ltac2/dune", line 5, characters 12-34:
5 | (libraries coq-core.plugins.ltac2))
^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.ltac2" not found.
Hint: try:
dune external-lib-deps --missing -p coq-stdlib @install
the hint doesn't seem to help. Is that expected?
Théo Zimmermann (Apr 29 2021 at 14:23):This is really weird. Why would dune install -p coq-core require anything but coq.install!?
Théo Zimmermann (Apr 29 2021 at 14:23):FTR I do see something quite similar (although different):
Théo Zimmermann (Apr 29 2021 at 14:23): dune install -p coq-core
Error: The following <package>.install are missing:
- _build/default/coq.install
- _build/default/coq-doc.install
Hint: try running: dune build @install
This really is not normal. It should be possible to build and install coq-core without building anything else.
Théo Zimmermann (Apr 29 2021 at 14:35):We should wait from confirmation from @Emilio Jesús Gallego Arias but IMHO this is a bug in Dune that should be reported.
Théo Zimmermann (Apr 29 2021 at 14:36):@Pierre Roux You can probably replace the call to dune install by opam-installer _build/default/coq-core.install.
Théo Zimmermann (Apr 29 2021 at 14:36):It should work since this is what the coq-core opam package does.
Théo Zimmermann (Apr 29 2021 at 14:38):I tested it with the additional --prefix=/tmp on my own machine and it worked.
Gaëtan Gilbert (Apr 29 2021 at 14:38):doesn't the pkg:opam job test this in CI?
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:42):Oh sorry, the doc is outdated
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:42):The right command is dune install $pkg
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:43):Previously dune install used to include dune build, so you could use the form dune install -p $pkg to mean dune build -p $pkg && dune install $pkg
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:44):but this was giving trouble now install is just a fully separate command and no build
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:44):indeed the man page for dune install needs work upstream
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:44):as it takes too many options which are not used anymore
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:45):IMHO it is a bug that dune install still takes all the options for dune build
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:45):but maybe they had to keep them for a while due to compat?
Théo Zimmermann (Apr 29 2021 at 17:51):It creates more trouble that they kept them while changing the meaning compared to just removing them.
Emilio Jesús Gallego Arias (Apr 29 2021 at 17:52):I would definitively submit a bug upstream tho it is likely there are some open as this change was a bit tricky
Jason Gross (Apr 30 2021 at 01:43):Was there a solution to "flock: failed to execute command: dune: No such file or directory" on Mac? Fiat-Crypto's Mac job suddenly broke, and copying Coq's Mac script doesn't seem to work. https://github.com/mit-plv/fiat-crypto/runs/2471237824?check_suite_focus=true
Michael Soegtrop (Apr 30 2021 at 11:03):What is flock btw?
Jason Gross (Apr 30 2021 at 11:04):I think it's how dune does locking of files so it can build things in parallel
Gaëtan Gilbert (Apr 30 2021 at 11:07):https://www.man7.org/linux/man-pages/man1/flock.1.html
Jason Gross (Apr 30 2021 at 11:29):Ah, apparently my problem is that make install used to work fine without OCaml in path, and now it fails if it can't find dune.
Pierre Roux (Apr 30 2021 at 13:13):@Emilio Jesús Gallego Arias how am I expected to build with coq-native? I tried ./configure -prefix <prefix> -native-compiler yes but the build then fails.
Emilio Jesús Gallego Arias (Apr 30 2021 at 13:28):@Jason Gross flock is only used by the make-dune bridge, indeed make needs to lock around dune calls [this is not needed if you are in a pure dune build] I assumed flock would be available easily in unix / cygwin but we can use the OSX native equivalent if we figure out which one it is.
make install requires dune as one of the big improvements is that we now delegate all the complex OCaml libraries install to dune build coq-core.install
Emilio Jesús Gallego Arias (Apr 30 2021 at 13:29):@Pierre Roux what error are you getting, the CI works fine, but note that indeed the pure dune build doesn't support native yet, will eventually do once we merge coqnative and Dune 2.9 is released.
Michael Soegtrop (Apr 30 2021 at 13:36):I see. On macOS flock is available as C function but not as shell command - unless installed via MacPorts / Homebrew. So I guess on macOS dune needs a depext dependency for flock.
Pierre Roux (Apr 30 2021 at 13:38):% ./configure -prefix <prefix> -native-compiler yes
% dune build -p coq-core
[...]
% dune install coq-core
% dune build -p coq-stdlib
coqdep theories/Floats/PrimFloat.v.d
*** Warning: in file Floats/PrimFloat.v, declared ML module float_syntax_plugin has not been found!
[...]
coqc theories/Init/.Ltac.aux,theories/Init/Ltac.{glob,vo} (exit 1)
[...]
File "./theories/Init/.coq-native/NCoq_Init_Ltac.native", line 1, characters 5-17:
Error: Unbound module Nativevalues
Error: Native compiler exited with status 2
This makes sense if native-compiler is not supported.
Pierre Roux (Apr 30 2021 at 13:40):Note however that coqnative is nice but the split-package approach still requires some amount of work on the opam repo side. There is no guarantee that this will be available for 8.14. So it would be safer to have a plan B supporting the coq-native OPAM virtual package approach as currently done with Coq 8.13.
Gaëtan Gilbert (Apr 30 2021 at 13:41):Michael Soegtrop said:
I see. On macOS flock is available as C function but not as shell command - unless installed via MacPorts / Homebrew. So I guess on macOS dune needs a depext dependency for flock.
not dune, it's the legacy build of coq that uses flock
Michael Soegtrop (Apr 30 2021 at 13:43):@Emilio Jesús Gallego Arias : as far as I can tell MacPorts does not provide a flock command, maybe homebrew does, but having to install homebrew just for that seems difficult. macOS has a somewhat similar command shlock.
It might be an option to write a simple flock command using the C command (which exists on macOS).
Emilio Jesús Gallego Arias (Apr 30 2021 at 13:44):@Michael Soegtrop if shlock is standard we can just detect it and use it on OSX
Emilio Jesús Gallego Arias (Apr 30 2021 at 13:46):@Pierre Roux actually there are two issues here:
make world && make install as beforedune build -p, if you wanna build two packages from the workspace that depend on each other you need to pass them both dune build -p coq-core,coq-stdlib Emilio Jesús Gallego Arias (Apr 30 2021 at 13:46):we should document both points better
Emilio Jesús Gallego Arias (Apr 30 2021 at 13:47):there is another option, which is to add (mode native) to stdlib/dune but this is not flexible enough so we didn't upstream it, and we are waiting for coqnative which indeed allows separate compilation so things are much easier to enable/disable.
Pierre Roux (Apr 30 2021 at 13:47):Thanks, maybe the first point is not worth documenting if it's gonna be fixed soon.
Emilio Jesús Gallego Arias (Apr 30 2021 at 13:51):@Théo Zimmermann I did make -f Makefile.dune world && _build/install/default/bin/coqtop and it seems to work, what problem you saw?
Michael Soegtrop (Apr 30 2021 at 17:12):@Emilio Jesús Gallego Arias : yes, as far as I can tell shlock is standard macOS. It lives in /usr/bin and has a BSD man page. So I would expect it is there since the BSD days. Btw.: shlock seems to be available on Linux as well, so you might be able to use shlock everywhere. See (https://linux.die.net/man/1/shlock).
Gaëtan Gilbert (Apr 30 2021 at 17:48):Bugs
shlock assumes that it will not be used in an environment with multiple locks/unlocks in a short time (due to a race condition). That is, shlock is intended for daily or hourly jobs.
Emilio Jesús Gallego Arias (Apr 30 2021 at 18:00):Indeed it seems that shlock doesn't work for our case, we can indeed build a small ocaml program using the opam flock package if we feel we need it.
Emilio Jesús Gallego Arias (Apr 30 2021 at 18:00):I am surprised tho flock is not is osx, but indeed it seems it only ships in iOS
Michael Soegtrop (May 01 2021 at 18:09):@Gaëtan Gilbert : I guess this Bugs section is from he Linux version. The BSD (or at least the Mac) version doesn't seem to have this. The Bugs section reads:
BUGS
Does not work on NFS or other network file system on different systems because the disparate systems
have disjoint PID spaces.
Cannot handle the case where a lock file was not deleted, the process that created it has exited, and
the system has created a new process with the same PID as in the dead lock file. The lock file will
appear to be valid even though the process is unrelated to the one that created the lock in the first
place. Always remove your lock files after you're done.
But of cause if OCaml supports it, it might be better to use that. The flock system call is available on macOS.
Yishuai Li (May 08 2021 at 02:47):Say I want to edit Coq master branch with Proof General on macOS. What should I do? I ran dune build @install (complaining No module named 'sphinx_rtd_theme'). How should I tell Emacs where to find the coqtop?
Emilio Jesús Gallego Arias (May 08 2021 at 13:26):@Yishuai Li , see the targets doing make -f Makefile.dune , you can run make -f Makefile.dune world and that will produce a full install layout in _build/install/default, you can point your coq-prog-name to that directory. If you are editing stdlib files, and include coq.el, then Proof General will pick as coqtop dev/shim/coqtop-prelude which is faster to build [using make -f Makefile.dune states
Yishuai Li (May 08 2021 at 22:31):Where's the coq.el file?
Emilio Jesús Gallego Arias (May 09 2021 at 00:08):Sorry the name is dev/tools/coqdev.el , see dev/README.md for more info
Last updated: Jun 08 2023 at 04:01 UTC