Emilio Jesús Gallego Arias (Jun 22 2022 at 19:01): Emilio Jesús Gallego Arias (Jun 22 2022 at 19:01):Hi folks, there was discussion in the hacking event w.r.t. the use cases of the newly implemented %{coq:version} variable. Two core questions that need feedback:
coq:version vs coq:release: I think that coq:release is the important one, like 8.15, 8.16, as people would like to use this variable for compat reasons mostly (and not often!) , is there a use for Coq version tho? coq:release allows you to do stuff like (copy_rules foo-%{coq:release} foo.v) easily, and that was my main motivation, but I don't know more.
Use cases. A good point raised in the meeting is that the use cases seem unclear. One use case is conditional compilation, but it was raised that a) conditional compilation could be implemented in Coq (but that's pretty costly) b) conditional compilation could be supported by some specialized stanza that would prevent user errors c) conditional compilation should be just discouraged.
What other uses cases for this variable we have?
Emilio Jesús Gallego Arias (Jun 22 2022 at 19:02):Thoughts?
Rudi Grinberg (Jun 22 2022 at 19:09):For version, I think you've listed all the potential use cases. We did not include the a discussion how coqc_config though. I think there are more use cases there - in particular, a way for coq to signal to dune which rules to setup and which features this compiler supports.
Emilio Jesús Gallego Arias (Jun 22 2022 at 19:29):Yes @Rudi Grinberg , for coq:config we have two cases that I know of:
coq:config:native to setup rules for Coq's vo to cmxs coq:config:lib to find the directory where the root of installed Coq libraries isI think that's all, coqc --config outputs a bit more stuff, so YMMV
Emilio Jesús Gallego Arias (Jun 22 2022 at 19:29):We also discussed quite a bit about allowing on demand native, which seems like a cool idea, but it makes sense to setup the rules the way coq_makefile does now for the immediate term (that is to say , Dune 3.4) , as the other part would require updates to Coq very likely
Ali Caglayan (Jun 22 2022 at 19:35):Here is my coq -config:
COQLIB=/mnt/sda1/.opam/coq.dev/lib/coq/
COQCORELIB=/mnt/sda1/.opam/coq.dev/lib/coq/../coq-core/
DOCDIR=/mnt/sda1/.opam/coq.dev/doc/coq/
OCAMLFIND=/mnt/sda1/.opam/coq.dev/bin/ocamlfind
CAMLFLAGS=-thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence
WARN=-warn-error +a-3
HASNATDYNLINK=true
COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQ_NATIVE_COMPILER_DEFAULT=yes
There is nothing there about vok/vos rules for example. That will have to be something that users enable themselves in a stanza
Ali Caglayan (Jun 22 2022 at 19:36):Apart from version and native, I don't really see many conditions the complication could use
Emilio Jesús Gallego Arias (Jun 22 2022 at 19:39):Ali Caglayan said:
There is nothing there about vok/vos rules for example. That will have to be something that users enable themselves in a stanza
I think we don't need to enable anything in the stanza for vos/vok, let's discuss on its own topic tho
Emilio Jesús Gallego Arias (Jun 22 2022 at 19:40):Ali Caglayan said:
Apart from version and native, I don't really see many conditions the complication could use
yes, we are tying to reduce config, so for now only native and coqlib
Rudi Grinberg (Jun 22 2022 at 20:11):Ali Caglayan said:
There is nothing there about vok/vos rules for example. That will have to be something that users enable themselves in a stanza
Once someone adds -no-vok to coqc, hopefully it will be reflected in coqc -config
Emilio Jesús Gallego Arias (Jun 22 2022 at 20:17):Rudi Grinberg said:
Ali Caglayan said:
There is nothing there about vok/vos rules for example. That will have to be something that users enable themselves in a stanza
Once someone adds
-no-voktocoqc, hopefully it will be reflected incoqc -config
why would they add that? There are no plans to add this I think.
Rudi Grinberg (Jun 22 2022 at 20:17):how would dune know when is -no-vok available for use?
Ali Caglayan (Jun 22 2022 at 20:19):coqc --help XDD
Ali Caglayan (Jun 22 2022 at 20:20):We could put it in coqc -config if implemented
Ali Caglayan (Jun 22 2022 at 20:20):The issue is that it is not so clear what we should be putting in coqc -config
Ali Caglayan (Jun 22 2022 at 20:21):atm it is just things that were passed during ./configure of coq
Rudi Grinberg (Jun 22 2022 at 20:21):as much things as possible really. The version, configuration options, the location of things, which capabilities are enabled.
Rudi Grinberg (Jun 22 2022 at 20:21):It's good to avoid having dune run multiple binaries to query for information
Ali Caglayan (Jun 22 2022 at 20:22):Why not deduce from the version?
Ali Caglayan (Jun 22 2022 at 20:22):If -no-vok gets implemented in 8.17 say, then it will be properly documented in coq
Ali Caglayan (Jun 22 2022 at 20:22):Then dune just has to check for the release version of coq rather than having to parse a whole config
Ali Caglayan (Jun 22 2022 at 20:25):On the other hand, I don't see any reason not to put it in the coq -config
Ali Caglayan (Jun 22 2022 at 20:26):However we might want to add existing features such as supported flags etc.
Ali Caglayan (Jun 22 2022 at 20:26):We could put them in coqc -config, but this would mean it won't work for older versions
Rudi Grinberg (Jun 22 2022 at 20:26):Versions are inferior.
Ali Caglayan (Jun 22 2022 at 20:29):We can start adding things in to config but there are two issues:
Ali Caglayan (Jun 22 2022 at 20:29):And its still not totally clear what "as much things as possible really" means
Ali Caglayan (Jun 22 2022 at 20:30):We need to come up with some sort of guideline on the Coq side for keeping it maintained
Rudi Grinberg (Jun 22 2022 at 20:30): Rudi Grinberg (Jun 22 2022 at 20:30):It's usually obvious when a change is interesting to a build system
Ali Caglayan (Jun 22 2022 at 20:31):But by that time, you would have missed support in older coq versions no?
Ali Caglayan (Jun 22 2022 at 20:31):I guess we could have a mix of version and config here. v1 v2 v3 support feature X, but v4 onwards has it explicitly stated in config or something?
Rudi Grinberg (Jun 22 2022 at 20:31):It doesn't matter. The absence of an entry means the feature is unavailable
Ali Caglayan (Jun 22 2022 at 20:32):For new features this is true
Ali Caglayan (Jun 22 2022 at 20:32):but what about things we already have
Rudi Grinberg (Jun 22 2022 at 20:33):We should assume those things are always present and only support coq >= 8.15
Gaëtan Gilbert (Jun 22 2022 at 20:34):what is -no-vok?
Rudi Grinberg (Jun 22 2022 at 20:35):Prevent coqc from producing those pesky empty .vok files
Emilio Jesús Gallego Arias (Jun 23 2022 at 13:17):capabilities are the way to go. For now only two things relevant in coq --config : native capabilities and coqlib location
Emilio Jesús Gallego Arias (Jun 23 2022 at 13:17):the rest are leftovers for Coq makefile, which should use it's own config system soon
Last updated: Oct 13 2024 at 01:02 UTC