Specify flag on file? · Coq users

Stream: Coq users

Topic: Specify flag on file?

Fernando Chu (Mar 28 2024 at 08:40):

Hello, is it possible to specify an argument/flag in a file? E.g. -arg -type-in-type. The intention being that students can use a library in jsCoq that requires this flag.

Meven Lennon-Bertrand (Mar 28 2024 at 09:18):

For this specific flag you can do Unset Universe Checking. which has the same effect. I don't know if all command-line flags have such an equivalent flag, but I would hope so.

Fernando Chu (Mar 28 2024 at 09:21):

Thank you!

Gaëtan Gilbert (Mar 28 2024 at 09:47):

rewrite rules (not yet in a released coq version), impredicative set, noinit are examples of command lines flags which don't have a corresponding Set

Karl Palmskog (Mar 28 2024 at 09:57):

would it even make sense to have a Set for impredicative set? It seems like a recipe for achieiving unsoundness quickly

Gaëtan Gilbert (Mar 28 2024 at 09:59):

and Unset Universe Checking isn't?

Pierre Courtieu (Mar 28 2024 at 10:23):

Is there a standard way of setting individual flags to specific files? I don't remember seeing this in coq_makefile's documentation. Maybe with dune?

Ali Caglayan (Apr 15 2024 at 16:48):

Pierre Courtieu said:

Is there a standard way of setting individual flags to specific files? I don't remember seeing this in coq_makefile's documentation. Maybe with dune?

We don't have per-file flags in dune.

Guillaume Melquiond (Apr 15 2024 at 17:09):

Pierre Courtieu said:

Is there a standard way of setting individual flags to specific files? I don't remember seeing this in coq_makefile's documentation. Maybe with dune?

I suppose you could add to file Makefile.coq.local a line

foo.vo: COQEXTRAFLAGS=whatever

Gaëtan Gilbert (Apr 15 2024 at 18:12):

that may set the variable for dependencies of foo though

Gaëtan Gilbert (Apr 15 2024 at 18:14):

you need private to be really specific to that file https://www.gnu.org/software/make/manual/make.html#Suppressing-Inheritance

Emilio Jesús Gallego Arias (Apr 16 2024 at 21:53):

Actually we could implement this in Dune easily, something like:

Emilio Jesús Gallego Arias (Apr 16 2024 at 21:55):

(coq.theory
  (name Foo)
  (flags
    (per_library
      (Bar.Muu (-w -some_thing_we_dont_want_here))))

Emilio Jesús Gallego Arias (Apr 16 2024 at 22:00):

It is a matter of:

extending the parser to create a map from Coq_lib_name.t -> Coq_Flags.t
in coq_rules.ml:261 there is a todo, there, we need to inject the flags doing the test with the map
we replace the current test for init with a test for flags in theories/dune, so no more hacks

Emilio Jesús Gallego Arias (Apr 17 2024 at 01:05):

https://github.com/ocaml/dune/pull/10429

Last updated: Oct 13 2024 at 01:02 UTC