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 -di
make -f Makefile.dune world
This 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?
git clean -xdff
is nuclear anihilation
What does repeating f
twice do?
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.
Git will refuse to modify untracked nested git repositories (directories with a .git subdirectory) unless a second -f is given.
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 -j4
andmake -f Makefile.dune world
) without having to call make clean or git clean anymore.
What is the difference between using these modes?
What should I do to have coqtop
back? Neither make
nor make -f Makefile.dune world
seem to have provided binaries (?)
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
binaries are in _build/install/default/bin
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)
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?
I concur that I don't know how to build coq_makefile in the current setup
@Ana de Almeida Borges how are you calling the test suite?
@Pierre-Marie Pédrot , dune build _build/install/default/bin/coq_makefile`
this would deserve an alias in the Makefile
@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.
or if using make make _build/install/default/bin/coq_makefile
@Ana de Almeida Borges make test-suite
should also work if you have done make world
before
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
I hadn't, I only did make
and make -f Makefile.dune world
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
I can't mangle my binaries, this breaks all developments in the wild
what do you mean @Pierre-Marie Pédrot ?
all scripts expect coq_makefile to be around
sure, I mean, how was around before?
before you had to add something to path
I can't expect scripts to call dune exec -- blah
oh sure, I didn't mean that for script use
most scripts expect the coq binaries to live in $COQBIN
then set COQBIN to _build/default/install/bin , and indeed execute the target you consider it proper
the test-suite: world
dep got removed?
@Emilio Jesús Gallego Arias that's what I did indeed, but I have to invoke building these tools expliclty
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
@Pierre-Marie Pédrot what target you used before?
to build a working set
@Gaëtan Gilbert it was not
my magic command line: make -j -l4 bin/coqc pluginsbyte tools miniopt coqide states printers bin/coqc.byte bin/coqchk miniopt states bin/coqchk
I guess there should be a tools
target for the wrapper makefile
hum, there is, but it doesn't compile coq_makefile
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.
best approximation you can do now is make coq-core.install
@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
.
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?
For your use case, I would just set the COQ_USE_DUNE
variable and use the targets there.
once you set that variable make
will be make -f Makefile.dune
@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
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.
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]
@Pierre-Marie Pédrot note that the tools
target is still in the makefile , but likely not building the right set of things
Yup, for some reason it is not included in tools, bugfix upcoming.
Ups, that should be make _build/default/coq-core.install
; opam / dune where updated so now install files are out of tree too
dune build coq-core.install
should still work though?
Yup, as dune interprets targets under _build
but for make we need to refer to the real file
unless we declare the target as phonhy
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
this is because if you call now binaries as _build_vo/default/bin/coqc
, the auto-magic we have works
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
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.
I am getting weird errors when trying to compile the ci targets locally.
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
the same error occurs with most developments
from what I gather, coq_makefile is not printing the right information to the output file which stays empty
i.e. in this example _build_ci/mathcomp/mathcomp/Makefile.coq
is empty when it should contain the autogenerated output
I confirm that coq_makefile does not output anything when run
without the -o
option it fails with Error: cannot find CoqMakefile.in
looks like yet another issue with coqlib since coq_makefile looks for that file somewhere under coqlib / tools
Yup, this is due to that file not being found. How did you configure Coq? I'll try to repro
CI doesn't test all possible combinations, I tried to do my best
Upcoming PRs do clean up the code handling the location of stuff, making it canonical
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
?
Also, exporting these in .bashrc
breaks coq when I change opam switches, which is not ideal. Do you have a workaround for it?
@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.
Oh, you are right. Thanks!
I am playing with the COQ_USE_DUNE setting, but it's even less functional than the hybrid make setting
with make states
, running coqc
results in an error Error: Cannot find plugins directory
and it doesn't solve https://github.com/coq/coq/issues/14187
also, I still need to set COQLIB otherwise coqc won't find it
what do?
Ah, right, my COQLIB was pointing to the wrong place (the _build_vo folder for hybrid mode instead of _build)
but I am still puzzled about what you said above @Emilio Jesús Gallego Arias
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
what setting do you recommend to make the binaries work?
(I can't use dune exec -- blah because all the scripts in the wild expect my binaries to be the vanilla coqc / whatever)
I just call the -prelude or install/ binaries directly
wdym?
as explained I have to set COQLIB otherwise it doesn't work
You are suggesting that -local is now replaced by make install?
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
but how do you compile external devs?
they expect coqc to be in the path
the _build/install/default/bin/coqc
also works for me, although I'm not sure what the minimal target for it is
please help, I am getting a bit desperate
even with a full world building I get the coqlib error
what specific commands from git clean?
also do you have any relevant variables set in your environment
export COQ_USE_DUNE=1
make world
I've tried removing all the COQ* variables to no avail
make world
errors?
no
what errors then
calling _build/install/default/bin/coqc
specific command please
this very command
wait a sec
I think I am messing up my environment variables
let me start again from scratch
in dune mode, from a clean state without crazy variables, make states
is not enough for coqc to work
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
https://github.com/coq/coq/blob/f4156a350f45e66c88c9cb2b12ce746e8aba3357/Makefile.dune#L17
what meaning "weird things"
CTRL-C, CTRL-D results in a not_found anomaly
first time I ever saw that
the backtrace tells me it's a parsing issue
what should I understand from your link?
coqtop doesn't work either
your shell or terminal inserts a special character for ^C I guess
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)
the states target is specifically for the shim coqtop
OK, but I don't want the shim
I want my good old binary
because the whole world expects this
then tell dune to build the binary
but the binary is here!
right
it's just not finding coqlib
my workaround was to export COQLIB which actually works
not that I really care, but I was promised a land of state-free environments
please standby I'm looking at the anomaly
(CTRL-C CTRL-D failing is not urgent, I can live with it)
(my setup not working is slightly more urgent)
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
it wants the prelude file and something with plugins, not sure of the specifics for plugins
can we get this added to the state
target then?
make a pr
I have no idea which file should be modified
whether Makefile.dune or the shim
or something else
Makefile.dune
I can make the pr if you prefer
wait a sec
still doesn't work actually
I get fancy errors when trying to compile external development with that
(it magically solved the coq_makefile issue for some reason)
Error: Cannot find library Coq.Init.Notations in loadpath
doesn't sound very good
where is that hidden state again
the miracle is that coqc
works but not coqtop
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
(indeed if you pass it a file to compile it dies with the same error)
x_x
I think that the problem is not so much in the build
rather, the loadpath initialization should handle this new situation
because there are two places where the library might be found
no, the problem is that dune is super annoying when you want minimal install targets
_build/default/theories/
and _build/install/default/lib/coq/theories
Actually after the -local PR there will be a single place so hopefully all this works much better
you want to setup a minimal working env for applications
you can do dune build coq-stdlib.install
and interrupt once it starts talking about non Init vo files
for that you want , all in _build/install
and add that to the path
just dune build _build/install/default/lib/coq/theories/Init/Prelude.vo
hm, but can't we have minimal install targets
yes you can
I am not going to type that every 20s in my terminal
the thing is that states
is only meant to be used from the shim
states
should build it for me
we can indeed reify it
adjust states so you get a install layout
the coq_makefile issue seems very related
so indeed you want a target that setups coq_makefile + states
?
coq_makefile should be set up by tools
I'd say don't pollute your env too much, just adjust path
states should build me a functional coqc / coqtop
the thing is that tools may build the stuff
(yeah, I tweak PATH depending on my needs)
but setting up the install layout is an extra step we may not be doing consistenly
and the code to locate stuff works over the install lyout
but that's not a biggy (even if annoying) adjusting some targets will do
I am fine with partial install targets being run in my back
yes, actually very soon I hope we will have the coqlib locate code handle more cases
the fact we are duplicating the build + install process looks like asking for trouble if you ask me
for example the library by Bobot in Dune to locate stuff works for both layouts
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?
Where is the duplication?
in the build and install directories, and that coqtop looks for both somewhat
coqtop is more dumb
install is just symlinks
actually you need something like install, as this is the stable layout on which clients of Coq can rely on
_build depends on how devs organize source code thus not stable
so there is not duplication per-se
just a rule that knows where to install things, which you ought to have anyways
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
in fact dune does that automatically if you setup a rule
depending on coqc
for example, if you write (run coqc foo.v)
also @Pierre-Marie Pédrot an instructive command to understand what dune does to the build env is dune exec -- env
we will soon have dune shell
which can drop you on a concrete env the rule is built on
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
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
as deps are tracked
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
that should be easy
can you confirm @Pierre-Marie Pédrot ?
Regarding @Enrico Tassi question, -local is not replaced by make install, but by having a install tree in _build_vo
so just make produces the stuff in _build_vo or _build/install/$context
In Dune, make world
will populate fully the install dir, so what we are missing is some smaller targets
nah, in general I don't want a precise vo files
most of the time, and this is what was done in the old makefile, I want to compile subfolders of theories/
like fset, zarith and whatnot
Ok I will add an example for a set of .vo files, then we can add the needed aliases
I tend to single out a file
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
can we get states to be fixed quickly?
it's my basic tool in daily dev and it's quite cumbersome currently to have to spell out the full prelude file
use the shim as a workaround, I think I will have a PR fixing all your problems today
oh sorry, the shim won't work for you
I can't use the shim because it won't work for external devs
I believe I can survive for 24 to 48h without trying to touch external developments
we could rename the shims to remove -prelude
yup, use the workaround of having to use an alias to dune build _build/install/default/.../foo.vo
until I submit the Pr
@Emilio Jesús Gallego Arias this doesn't work for the prelude because it doesn't install all the files
I'd need to explicitly list all the vo from the prelude
tbh I'd like a dune command to say "put everything you can into install/ without building anything new"
https://github.com/coq/coq/pull/14201
isn't the reliance on the shell going to wreak havoc when passing quoted arguments?
we can fix the quoting (added to pr)
do I understand correctly this is a short-term solution?
ideally I should just have to add the install binary folder to my PATH, right?
not the shim one
yes
I didn't actually test adding the shims to PATH so it might not even work tbh
but the -prelude suffix is useless imo so we may as well remove it regardless
@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
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
etc...
let me work a bit on the POC to solve your immediate problem
(also coq_makefile is not part of the shims, so this is not going to solve that problem)
full dune build is not dying on coqc warnings, is that expected?
(also the colouring of warning is not preserved by the dune compilation wrapper, I believe we should probably pass an explicit option to coqc)
No, I think this is unexpected.
the hybrid make does fail on warning, that said
Sure, but this is completely independant.
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?
Last woe is CoqIDE being unable to find the stdlib
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
I must be missing something because this is literally one of the first thing you do when you write a patch.
What do you people do?
I can't make world or whatever because precisely it does not compile
what did you try?
(and I am not going to ask dune by hand to put the vo files in the install subdirectory)
what should I try?
make world fails
I want to fix the stdlib, so I launch CoqIDE
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
regardless of whether I use the shim or not
what am I doing wrong?
we don't have a target to ask for those vo files to be moved to install
please help because in the last 48h or so my mental sanity has been taking a heavy toll
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)
but I can't edit
coqide fails on Require
because the vo files are not at the right place
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
???
did you run the file in CoqIDE?
y
it fails on Require
n
I did the very same thing.
(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)
let's try in pure dune mode
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
I use -profile devel
which probably sets local?
y
OK, so it works in pure dune mode
(the problem with pure dune mode is that many useful targets are missing)
the shims are only for pure dune mode to be clear
right.
so IIUC hybrid mode + local is broken
because none of the tools are able to resolve COQLIB in a meaningful way
(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.)
you can add -w +default
to the flags
in theories/dune
I don't know if it should always be enabled or conditionally somehow
why don't we have a configure in dune mode? It's typically used for that
:shrug:
ok, no questions asked
we could make that a configure thing indeed and include the flags in the dune file
my workflow is like this @Pierre-Marie Pédrot
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
yes, I had intuited that messing with COQLIB was a bad idea
that is indeed not very well supported yet
as when I wanted to run ci-*
I do make world
and how do you modify external developments?
so things work fine for my workflow
I just do make world, then for plugins, they are already dunerized
so just uncomment the (dirs )
line dune
and the make check
will include the plugins in ci-
for .v files, I am working on having all of ci dunerized too
so I don't have to care, I can just do dune build whatever.vo
and I get a minimal rebuild
for now I have been relying on world
I but I have an approach where I never try to outdo the build system
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
I'll try to stay away from the hybrid mode, it seems to be broken for dev purposes
I'll make things much better once coq.boot goes in
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
that's what I use all the time
check
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
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
I don't think you can solve slow Coq build times by tweaking the build system, but well
Oh we could improve a lot, if you look at trace file that dune generates
in my 4 core / 8 threads machine there is room for improvement
I mean, I am talking about vo files that take > 10mn to compile
contrarily to the typical OCaml file, Coq compilation is not IO-bound
Yup but when you have 8 cores, there is a lot of contention in our current build
mathcomp is pretty terrible for instance
Indeed if you are gonna hack on math-comp you better get a beefy computer
but in terms of what make world takes, we got like a minute in my computer of margin to make it faster
there was a couple of terrible files
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
there is still coqdep taking ages on stdlib
That's fixed in 2.9 , 20 secs less
I mean, not at boot, just when recompiling a file
Indeed I should have fixed that by now
yes I know, that was a bad design decision
yes, I've seen some issue posted
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
cache does alleviate that to some extend
Please open the bug regading the make setup so I'm sure coq-boot does fix it
if it's expected that the hybrid setup doesn't work with the shim, it's not a bug?
hybrid setup should work by calling the binaries directly
"as before"
After https://github.com/coq/coq/pull/14176 using _build_vo/default/bin/coqc for example
bin directory is used so we could indeed have it created as a symlink
is not used now I mean
indeed the shims will set coqlib to where the object files for the regular dune build work
we could have them test if _build_vo exists and then use that, I dunno
but then I think it's just the same bug as before, i.e. COQLIB is wrong
yup that's a bug that's why we need the PR
I mean that there is no point in opening an issue, we already have one opened for that
well in my testing the binaries were finding coqlib, but indeed there are couple of cases where it doesn't work
there are separate issues I think, but indeed, no need open if you want the problem is known
I will wait for the dust to settle a bit and open issues if the problems persist despite the relevant PRs being merged
but assume $bin points to the directory where binaries are, then make states && $bin/coqc
should work like before
if it doesn't it is a bug
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...
hm, I am a bit confused now
As a dev I shouldn't use the hybrid mode
so I am not sure of the usefulness of supporting this kind of dev setup
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?
This is really weird. Why would dune install -p coq-core
require anything but coq.install
!?
FTR I do see something quite similar (although different):
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.
We should wait from confirmation from @Emilio Jesús Gallego Arias but IMHO this is a bug in Dune that should be reported.
@Pierre Roux You can probably replace the call to dune install
by opam-installer _build/default/coq-core.install
.
It should work since this is what the coq-core opam package does.
I tested it with the additional --prefix=/tmp
on my own machine and it worked.
doesn't the pkg:opam
job test this in CI?
Oh sorry, the doc is outdated
The right command is dune install $pkg
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
but this was giving trouble now install is just a fully separate command and no build
indeed the man page for dune install needs work upstream
as it takes too many options which are not used anymore
IMHO it is a bug that dune install still takes all the options for dune build
but maybe they had to keep them for a while due to compat?
It creates more trouble that they kept them while changing the meaning compared to just removing them.
I would definitively submit a bug upstream tho it is likely there are some open as this change was a bit tricky
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
What is flock
btw?
I think it's how dune does locking of files so it can build things in parallel
https://www.man7.org/linux/man-pages/man1/flock.1.html
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.
@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.
@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
@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.
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.
% ./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.
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.
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
@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).
@Michael Soegtrop if shlock
is standard we can just detect it and use it on OSX
@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
we should document both points better
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.
Thanks, maybe the first point is not worth documenting if it's gonna be fixed soon.
@Théo Zimmermann I did make -f Makefile.dune world && _build/install/default/bin/coqtop
and it seems to work, what problem you saw?
@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).
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.
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.
I am surprised tho flock is not is osx, but indeed it seems it only ships in iOS
@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.
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
?
@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
Where's the coq.el
file?
Sorry the name is dev/tools/coqdev.el
, see dev/README.md
for more info
Last updated: Jun 08 2023 at 04:01 UTC