Stream: Coq users

Topic: Specify flag on file?


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

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

view this post on Zulip Fernando Chu (Mar 28 2024 at 09:21):

Thank you!

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

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

view this post on Zulip Gaëtan Gilbert (Mar 28 2024 at 09:59):

and Unset Universe Checking isn't?

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

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

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

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

that may set the variable for dependencies of foo though

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 16 2024 at 21:53):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 16 2024 at 22:00):

It is a matter of:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 17 2024 at 01:05):

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


Last updated: Jun 22 2024 at 16:02 UTC