Stream: Dune devs & users

Topic: coq:version variable


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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 22 2022 at 19:02):

Thoughts?

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

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

I think that's all, coqc --config outputs a bit more stuff, so YMMV

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

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

view this post on Zulip Ali Caglayan (Jun 22 2022 at 19:35):

There is nothing there about vok/vos rules for example. That will have to be something that users enable themselves in a stanza

view this post on Zulip Ali Caglayan (Jun 22 2022 at 19:36):

Apart from version and native, I don't really see many conditions the complication could use

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

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

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

view this post on Zulip 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-vok to coqc, hopefully it will be reflected in coqc -config

why would they add that? There are no plans to add this I think.

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:17):

how would dune know when is -no-vok available for use?

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:19):

coqc --help XDD

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:20):

We could put it in coqc -config if implemented

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

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:21):

atm it is just things that were passed during ./configure of coq

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

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:21):

It's good to avoid having dune run multiple binaries to query for information

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:22):

Why not deduce from the version?

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

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

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

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:26):

However we might want to add existing features such as supported flags etc.

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

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:26):

Versions are inferior.

  1. It requires bumping the version in development
  2. The user must now downgrade to disable/enable features.
  3. It doesn't work well when developing two features that require a new version at once

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:29):

We can start adding things in to config but there are two issues:

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:29):

And its still not totally clear what "as much things as possible really" means

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

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:30):

  1. When an entry is missing in coqc -config, we assume that's the same as being disabled/unsupported
  2. Hopefully as early as possible.

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:30):

It's usually obvious when a change is interesting to a build system

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:31):

But by that time, you would have missed support in older coq versions no?

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

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:31):

It doesn't matter. The absence of an entry means the feature is unavailable

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:32):

For new features this is true

view this post on Zulip Ali Caglayan (Jun 22 2022 at 20:32):

but what about things we already have

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:33):

We should assume those things are always present and only support coq >= 8.15

view this post on Zulip Gaëtan Gilbert (Jun 22 2022 at 20:34):

what is -no-vok?

view this post on Zulip Rudi Grinberg (Jun 22 2022 at 20:35):

Prevent coqc from producing those pesky empty .vok files

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

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC