Stream: Coq devs & plugin devs

Topic: coq-core and coq-stdlib opam packages

Lasse Blaauwbroek (Apr 20 2021 at 10:48):

It would be nice if we could add Opam packages in the coq-core-dev repo for coq-core and coq-stdlib. I can make a pull request for this, but I don´t know if there are any strong opinions about using the opam files automatically generated by dune. Would it be a problem to switch from the make-based system to the dune-based system for opam?

Emilio Jesús Gallego Arias (Apr 20 2021 at 11:02):

I think for coq-core you can use the opam file, for coq-stdlib I'd use the make call, as we didn't merge the support for the native compute separate compiler yet. You may want to wait until we merge https://github.com/coq/coq/pull/13617 tho.

Lasse Blaauwbroek (Apr 20 2021 at 11:14):

Ah looks like that will merge soon. I´ll indeed wait.

Lasse Blaauwbroek (Aug 29 2021 at 22:21):

Given that https://github.com/coq/coq/pull/13617 was merged long ago, I'm trying to prepare a PR to finally have the package split in the opam repo. One issue I'm not sure how to resolve is dealing with the coq-native package/flag. How do I incorporate this into opam files generated by dune?

Pierre Roux (Aug 30 2021 at 06:11):

You probably just heva to keep the configure call into the coq-core package.

Lasse Blaauwbroek (Aug 30 2021 at 08:00):

Ah, okay I'll try that. Thanks

Théo Zimmermann (Aug 30 2021 at 09:37):

I don't think it's yet possible to do the split in the opam repo because the full Dune build does not support native compilation of the standard library yet.

Lasse Blaauwbroek (Aug 30 2021 at 09:47):

Théo Zimmermann said:

I don't think it's yet possible to do the split in the opam repo because the full Dune build does not support native compilation of the standard library yet.

Ah, okay. I was not aware of that. I just opened this PR: https://github.com/coq/opam-coq-archive/pull/1801

Emilio Jesús Gallego Arias (Aug 30 2021 at 10:49):

Indeed, the make-based build for the .vo parts does not support using installed Coq to compile, tho, that should be very easy to work around, you just need to tweak the makefiles so COQC COQDEP and a couple of other tools are taken from the installed path

Lasse Blaauwbroek (Aug 30 2021 at 13:21):

@Emilio Jesús Gallego Arias I tried changing CBIN in Makefile.common to point to the installed binaries, but this does not work. I also tried changing CONTEXT and BCONTEXT, but it makes no difference.

$ make -f Makefile.make coqlib
make --warn-undefined-variable --no-builtin-rules -f Makefile.build coqlib
make[1]: Entering directory '/home/lasse/Documents/Projects/Tactician/tmp-split/coq'
DUNE      sources
DUNE      /home/lasse/Documents/Projects/Tactician/tmp-split/_opam/bin//coqc
COQCBOOT  theories/Init/Notations.v
DUNE      _build/default/plugins/ltac/ltac_plugin.cmxs
COQCBOOT  theories/Init/Ltac.v
File "./_build_vo/default//lib/coq/theories/Init/Ltac.v", line 11, characters 0-32:
Error: Dynlink error: implementation mismatch on Stdarg

make[1]: *** [Makefile.build:333: _build_vo/default//lib/coq/theories/Init/Ltac.vo] Error 1
make[1]: *** [_build_vo/default//lib/coq/theories/Init/Ltac.vo] Deleting file '_build_vo/default//lib/coq/theories/Init/Ltac.glob'

Lasse Blaauwbroek (Aug 30 2021 at 13:52):

Mhm, okay that error was due to some old files left lying around. But I tried running the coqlib target with a completely unmodified version of master, and that also does not work:

$ make -f Makefile.make coqlib
make --warn-undefined-variable --no-builtin-rules -f Makefile.build coqlib
make[1]: Entering directory '/home/lasse/Documents/Projects/Tactician/tmp-split/coq'
DUNE      _build/install/default/bin/coqdep
DUNE      sources
COQDEP    VFILES
DUNE      sources
DUNE      _build/install/default/bin/coqc
COQCBOOT  theories/Init/Notations.v
Error: Cannot find plugins directory

Looks like the plugins directory ends up in _build, while the make file expects it to be in _build_vo

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:13):

Umm, you need to patch things a bit more, in particular when, let's say, building from an installed coq-core package, the makefiles should:

• not build any binary stuff, such as plugins or coqdep
• set coqlib properly, but I wonder if that's gonna fly properly due to restrictions on make setup, for example the following plugins check, so maybe you need to do a symbolic link to the installed plugins file and then set coqlib to _build_vo

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:13):

_build should not be involved at all here

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:13):

actually there is this Draft PR switching the build of the stdlib to coq makefile

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:13):

maybe that would be a quicker path

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:14):

to tweak this, I'd advise to define a BUILD_VO_FROM_INSTALLED_COQ make var

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:14):

and just wrap everything in the bridge file [common] there

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:14):

so you start with a kind of "minimal" make file for the VO files

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:14):

then you just need to setup the copy of the files

Emilio Jesús Gallego Arias (Aug 30 2021 at 18:14):

and the couple of binary paths for COQDEP and COQC

Lasse Blaauwbroek (Aug 30 2021 at 18:55):

I see, that sounds like quite a few changes will be needed. I was hoping to have this for 8.14, but this sounds like that would probably not be possible. (Let me know if I'm wrong). If we are targetting 8.15, and a lot of changes need to be done, and you'd like me to be involved, it might be a good idea to have a bit more coordination on it (instead of me just hacking away on it randomly).

Last updated: Jun 05 2023 at 09:01 UTC