Stream: Coq devs & plugin devs

Topic: Using dune


view this post on Zulip 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:

  1. Confirm I have dune installed with dune --version
  2. Create ~/.config/dune/config with contents
(lang dune 2.8)
(cache enabled)
  1. Pull the most recent commits from coq master
  2. make clean and git clean -di
  3. 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?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 13:29):

git clean -xdff is nuclear anihilation

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 13:35):

What does repeating f twice do?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 -j4 and make -f Makefile.dune world) without having to call make clean or git clean anymore.

What is the difference between using these modes?

view this post on Zulip 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 (?)

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 13:48):

binaries are in _build/install/default/bin

view this post on Zulip 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/

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 13:49):

(adapt to your system)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:24):

@Ana de Almeida Borges how are you calling the test suite?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:26):

@Pierre-Marie Pédrot , dune build _build/install/default/bin/coq_makefile`

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:26):

this would deserve an alias in the Makefile

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:26):

or if using make make _build/install/default/bin/coq_makefile

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (Apr 27 2021 at 14:27):

I hadn't, I only did make and make -f Makefile.dune world

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:28):

I can't mangle my binaries, this breaks all developments in the wild

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:28):

what do you mean @Pierre-Marie Pédrot ?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:29):

all scripts expect coq_makefile to be around

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:29):

sure, I mean, how was around before?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:30):

before you had to add something to path

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:30):

I can't expect scripts to call dune exec -- blah

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:30):

oh sure, I didn't mean that for script use

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:30):

most scripts expect the coq binaries to live in $COQBIN

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 14:31):

the test-suite: world dep got removed?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:32):

@Pierre-Marie Pédrot what target you used before?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:33):

to build a working set

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:33):

@Gaëtan Gilbert it was not

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:34):

I guess there should be a tools target for the wrapper makefile

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 14:34):

hum, there is, but it doesn't compile coq_makefile

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:38):

best approximation you can do now is make coq-core.install

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:41):

once you set that variable make will be make -f Makefile.dune

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:47):

Yup, for some reason it is not included in tools, bugfix upcoming.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 14:54):

dune build coq-core.install should still work though?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:56):

Yup, as dune interprets targets under _build

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:56):

but for make we need to refer to the real file

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 14:57):

unless we declare the target as phonhy

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 17:45):

I am getting weird errors when trying to compile the ci targets locally.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 17:46):

this is after make world

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 17:48):

the same error occurs with most developments

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 17:51):

I confirm that coq_makefile does not output anything when run

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 17:52):

without the -ooption it fails with Error: cannot find CoqMakefile.in

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 18:19):

CI doesn't test all possible combinations, I tried to do my best

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Apr 27 2021 at 18:36):

Oh, you are right. Thanks!

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:24):

with make states, running coqc results in an error Error: Cannot find plugins directory

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:24):

and it doesn't solve https://github.com/coq/coq/issues/14187

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:26):

also, I still need to set COQLIB otherwise coqc won't find it

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:26):

what do?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:46):

what setting do you recommend to make the binaries work?

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:49):

I just call the -prelude or install/ binaries directly

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:49):

wdym?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:49):

as explained I have to set COQLIB otherwise it doesn't work

view this post on Zulip Enrico Tassi (Apr 28 2021 at 11:49):

You are suggesting that -local is now replaced by make install?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:50):

ie instead of previously make states; bin/coqc bla I do dune build dev/shim/coqtop-prelude; _build/default/dev/shim/coqtop-prelude

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:51):

but how do you compile external devs?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:51):

they expect coqc to be in the path

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:53):

please help, I am getting a bit desperate

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:53):

even with a full world building I get the coqlib error

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:54):

what specific commands from git clean?

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:55):

also do you have any relevant variables set in your environment

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:55):

export COQ_USE_DUNE=1
make world

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:55):

I've tried removing all the COQ* variables to no avail

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:55):

make world errors?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:55):

no

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:56):

what errors then

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:56):

calling _build/install/default/bin/coqc

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 11:56):

specific command please

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:56):

this very command

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:57):

wait a sec

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:57):

I think I am messing up my environment variables

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 11:58):

let me start again from scratch

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:01):

also dune exec -- dev/shim/coqtop-prelude does weird things

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:02):

https://github.com/coq/coq/blob/f4156a350f45e66c88c9cb2b12ce746e8aba3357/Makefile.dune#L17

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:02):

what meaning "weird things"

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:02):

CTRL-C, CTRL-D results in a not_found anomaly

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:03):

first time I ever saw that

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:03):

the backtrace tells me it's a parsing issue

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:04):

what should I understand from your link?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:04):

coqtop doesn't work either

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:04):

your shell or terminal inserts a special character for ^C I guess

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:04):

(maybe for the shell, but it didn't do that before, I regularly CTRL-C CTRL-D to quit coqtop)

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:04):

the states target is specifically for the shim coqtop

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:05):

OK, but I don't want the shim

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:05):

I want my good old binary

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:05):

because the whole world expects this

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:06):

then tell dune to build the binary

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:06):

but the binary is here!

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:06):

right

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:06):

it's just not finding coqlib

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:07):

my workaround was to export COQLIB which actually works

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:07):

please standby I'm looking at the anomaly

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:08):

(CTRL-C CTRL-D failing is not urgent, I can live with it)

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:08):

(my setup not working is slightly more urgent)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:14):

can we get this added to the state target then?

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:14):

make a pr

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:15):

I have no idea which file should be modified

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:15):

whether Makefile.dune or the shim

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:15):

or something else

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:15):

Makefile.dune

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:16):

I can make the pr if you prefer

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:16):

wait a sec

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:17):

still doesn't work actually

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:17):

I get fancy errors when trying to compile external development with that

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:17):

(it magically solved the coq_makefile issue for some reason)

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:18):

Error: Cannot find library Coq.Init.Notations in loadpath

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:18):

doesn't sound very good

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:18):

where is that hidden state again

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:19):

the miracle is that coqc works but not coqtop

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:20):

coqc is silent in the same state

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:22):

x_x

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:22):

I think that the problem is not so much in the build

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:23):

rather, the loadpath initialization should handle this new situation

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:23):

because there are two places where the library might be found

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:23):

no, the problem is that dune is super annoying when you want minimal install targets

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:23):

_build/default/theories/ and _build/install/default/lib/coq/theories

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:23):

you want to setup a minimal working env for applications

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):

for that you want , all in _build/install

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):

and add that to the path

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):

just dune build _build/install/default/lib/coq/theories/Init/Prelude.vo

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:24):

hm, but can't we have minimal install targets

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:24):

yes you can

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:24):

I am not going to type that every 20s in my terminal

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:25):

states should build it for me

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):

we can indeed reify it

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):

adjust states so you get a install layout

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:25):

the coq_makefile issue seems very related

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):

so indeed you want a target that setups coq_makefile + states

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):

?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:25):

coq_makefile should be set up by tools

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:25):

I'd say don't pollute your env too much, just adjust path

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:26):

states should build me a functional coqc / coqtop

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:26):

the thing is that tools may build the stuff

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:26):

(yeah, I tweak PATH depending on my needs)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:26):

and the code to locate stuff works over the install lyout

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:27):

I am fine with partial install targets being run in my back

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:28):

Where is the duplication?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:29):

in the build and install directories, and that coqtop looks for both somewhat

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):

coqtop is more dumb

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):

install is just symlinks

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):

_build depends on how devs organize source code thus not stable

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:30):

so there is not duplication per-se

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):

in fact dune does that automatically if you setup a rule

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):

depending on coqc

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:32):

for example, if you write (run coqc foo.v)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:35):

as deps are tracked

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:36):

that should be easy

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:36):

can you confirm @Pierre-Marie Pédrot ?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:38):

so just make produces the stuff in _build_vo or _build/install/$context

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:39):

nah, in general I don't want a precise vo files

view this post on Zulip 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/

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:40):

like fset, zarith and whatnot

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:43):

I tend to single out a file

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:45):

can we get states to be fixed quickly?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 12:47):

oh sorry, the shim won't work for you

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:47):

I can't use the shim because it won't work for external devs

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:48):

we could rename the shims to remove -prelude

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 12:49):

I'd need to explicitly list all the vo from the prelude

view this post on Zulip 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"

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:52):


https://github.com/coq/coq/pull/14201

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 12:58):

we can fix the quoting (added to pr)

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 13:00):

do I understand correctly this is a short-term solution?

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2021 at 13:00):

not the shim one

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 28 2021 at 13:01):

but the -prelude suffix is useless imo so we may as well remove it regardless

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 13:02):

etc...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2021 at 13:02):

let me work a bit on the POC to solve your immediate problem

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 10:21):

full dune build is not dying on coqc warnings, is that expected?

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 11:30):

No, I think this is unexpected.

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 11:49):

the hybrid make does fail on warning, that said

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 11:58):

Sure, but this is completely independant.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:22):

Last woe is CoqIDE being unable to find the stdlib

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:23):

What do you people do?

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:24):

I can't make world or whatever because precisely it does not compile

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 12:25):

what did you try?

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:25):

what should I try?

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:25):

make world fails

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:25):

I want to fix the stdlib, so I launch CoqIDE

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:25):

CoqIDE fails because the depending vo files are not in the path

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:26):

regardless of whether I use the shim or not

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:26):

what am I doing wrong?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:28):

but I can't edit

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:28):

coqide fails on Require

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:28):

because the vo files are not at the right place

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:31):

???

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:31):

did you run the file in CoqIDE?

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 12:31):

y

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:31):

it fails on Require

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 12:31):

n

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:31):

I did the very same thing.

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:32):

let's try in pure dune mode

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:35):

I use -profile devel which probably sets local?

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 12:36):

y

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:36):

OK, so it works in pure dune mode

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:37):

(the problem with pure dune mode is that many useful targets are missing)

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 12:37):

the shims are only for pure dune mode to be clear

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:37):

right.

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:37):

so IIUC hybrid mode + local is broken

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:38):

because none of the tools are able to resolve COQLIB in a meaningful way

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 12:50):

:shrug:

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 12:51):

ok, no questions asked

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:02):

my workflow is like this @Pierre-Marie Pédrot

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:02):

dune build theories/foo.vo
dune exec -- dev/shim/coq{c,ide} etc...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:02):

works pretty well, note that I don't set coqlib to the install path

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:03):

yes, I had intuited that messing with COQLIB was a bad idea

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):

that is indeed not very well supported yet

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):

as when I wanted to run ci-*

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):

I do make world

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:03):

and how do you modify external developments?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:03):

so things work fine for my workflow

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):

I just do make world, then for plugins, they are already dunerized

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):

so just uncomment the (dirs ) line dune

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):

and the make check

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):

will include the plugins in ci-

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:04):

for .v files, I am working on having all of ci dunerized too

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:05):

for now I have been relying on world

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:07):

I'll make things much better once coq.boot goes in

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08):

that's what I use all the time

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08):

check

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:08):

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:12):

in my 4 core / 8 threads machine there is room for improvement

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:12):

I mean, I am talking about vo files that take > 10mn to compile

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:12):

contrarily to the typical OCaml file, Coq compilation is not IO-bound

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:13):

mathcomp is pretty terrible for instance

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:15):

there was a couple of terrible files

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:16):

there is still coqdep taking ages on stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:17):

That's fixed in 2.9 , 20 secs less

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:17):

I mean, not at boot, just when recompiling a file

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:17):

Indeed I should have fixed that by now

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:17):

yes I know, that was a bad design decision

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:18):

yes, I've seen some issue posted

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:22):

cache does alleviate that to some extend

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:30):

hybrid setup should work by calling the binaries directly

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:30):

"as before"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:31):

is not used now I mean

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:33):

yup that's a bug that's why we need the PR

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 13:35):

if it doesn't it is a bug

view this post on Zulip 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...

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:36):

hm, I am a bit confused now

view this post on Zulip Pierre-Marie Pédrot (Apr 29 2021 at 13:37):

As a dev I shouldn't use the hybrid mode

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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!?

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 14:23):

FTR I do see something quite similar (although different):

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 14:31):

This really is not normal. It should be possible to build and install coq-core without building anything else.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 14:36):

It should work since this is what the coq-core opam package does.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 14:38):

I tested it with the additional --prefix=/tmp on my own machine and it worked.

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 14:38):

doesn't the pkg:opam job test this in CI?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 17:42):

Oh sorry, the doc is outdated

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 17:42):

The right command is dune install $pkg

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 17:44):

indeed the man page for dune install needs work upstream

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 17:44):

as it takes too many options which are not used anymore

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2021 at 17:45):

but maybe they had to keep them for a while due to compat?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 30 2021 at 11:03):

What is flock btw?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 30 2021 at 11:07):

https://www.man7.org/linux/man-pages/man1/flock.1.html

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 13:46):

@Pierre Roux actually there are two issues here:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 13:46):

we should document both points better

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Apr 30 2021 at 13:47):

Thanks, maybe the first point is not worth documenting if it's gonna be fixed soon.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (May 01 2021 at 18:10):

But of cause if OCaml supports it, it might be better to use that. The flock system call is available on macOS.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yishuai Li (May 08 2021 at 22:31):

Where's the coq.el file?

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (May 27 2021 at 15:47):

I realize that other people have asked similar things, but I'm still stuck. I want to locally run CI for some projects, eg mathcomp. From a fresh coq clone:

export COQ_USE_DUNE=true
make world
make ci-mathcomp

leads to

[...]
+ command make
make[1]: Entering directory '/home/ana/coq/_build_ci/mathcomp/mathcomp'
/home/ana/coq/_build/install/default/bin/coq_makefile  -f Make -o Makefile.coq
make -f Makefile.coq --no-print-directory
COQC ssreflect/ssreflect.v
/bin/sh: 1: time: not found
make[3]: *** [Makefile.coq:763: ssreflect/ssreflect.vo] Error 127
make[2]: *** [Makefile.coq:386: all] Error 2
make[1]: *** [Makefile.common:99: this-build] Error 2
make[1]: Leaving directory '/home/ana/coq/_build_ci/mathcomp/mathcomp'
make: *** [Makefile.ci:110: ci-mathcomp] Error 2

I do have the command time working, which was my only guess after reading the error. This is with OCaml 4.12.0.
As extra examples, the same strategy works with ci-flocq and fails with ci-bignums


Last updated: Oct 16 2021 at 02:03 UTC