Stream: Dune devs & users

Topic: dune rule for coqchk?


view this post on Zulip Ali Caglayan (Nov 15 2021 at 14:41):

What is the best way to do a coq_makefile-style validate with dune? Obviously, it is not currently supported but is there a way to write a rule or something?

view this post on Zulip Ali Caglayan (Nov 15 2021 at 14:43):

ping @Emilio Jesús Gallego Arias

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 14:44):

something like

(rule (alias validate)
  (deps $all_vo_files$)
  (action (run coqchk -some-Q %{deps}))

I guess

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 14:45):

(for the right values of $all_vo_files$ and -some-Q)

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:46):

ah, but doesn't this cause the (in)famous coqchk re-checking of everything in each call?

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:47):

You mean because by default dune builds everything?

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 14:48):

Karl Palmskog said:

ah, but doesn't this cause the (in)famous coqchk re-checking of everything in each call?

is that different from coq_makefile?

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:48):

but coq_makefile builds artifacts that are not built twice

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:49):

since there are no corresponding files generated by coqchk, it does work from ground up for every file, right?

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 14:49):

coqchk doesn't build artifacts

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:49):

Validate runs on the whole project both above and in coq_makefile

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:49):

But only when you call the appropriate target

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:50):

for example, say that you have a dependency chain:
lib.v -> A.v -> Top.v.

Then calling coqchk on lib.vo and A.vo would be redundant if you do coqchk Top.vo. I believe Emilio has suggested one should generate lib.ok and A.ok or something to avoid this.

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 14:51):

the pseudo rule I posted and coq_makefile just do 1 call coqchk lib.vo A.vo Top.vo so no redundancy

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 14:52):

you can't trust a .ok file anyway

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:52):

there’s an option to change this, but by default coqchk rechecks proof terms for your project _and its dependencies_ (including the stdlib), so you run it once on everything, and you rerun it if anything changes.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 14:52):

well, you can trust it if you generate it yourself

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:52):

(so the rerunning is not so frequent)

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 14:53):

you’re probably thinking more of the -non-rec option (or whatever it’s called) which trusts proof terms from dependencies?

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:11):

OK that seemed to work

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:11):

I'm depending on my vo files like this: (deps (glob_files *.vo))

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:12):

Is there a better way to do this?

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:12):

Can I just tell dune to look for vo files that come from src?

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 15:12):

vo files that come from src

glob_files src/*.vo?

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 15:13):

if you have subdirectories take care as glob_files doesn't recurse

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:13):

I have quite a few subdirectories

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 15:14):

then you need quite a few globs

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:15):

glob_files recurse but not sure if only in 3.0

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:15):

is called glob_files_rec, note that what Gaëtan wrote is incremental still, the alias will be considered up to date [if the exit code was fine] until the deps change

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:17):

Can't find anything in the refman about glob_files_rec I'm guessing that is new

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:18):

I'm confused tho, I would have thought (deps (glob_files src/**/*.vo)) would work but it doesn't seem to

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:20):

Also glob_files src/*.vo doesn't seem to do anything either

view this post on Zulip Gaëtan Gilbert (Nov 15 2021 at 15:21):

Ali Caglayan said:

I'm confused tho, I would have thought (deps (glob_files src/**/*.vo)) would work but it doesn't seem to

anything before the last / is taken as a literal path

probably you don't have a src/** directory

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:22):

Seems to be 3.0 only ? https://dune.readthedocs.io/en/latest/concepts.html#glob

There is a very unfortunate issue with the Dune manual https://github.com/ocaml/dune/issues/4982

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:23):

Yes, (glob_files ...) is a bit strange, in the sense it only understands a single directory

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:23):

OK let me start over then

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:23):

I have a src directory

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:23):

with multiple .v files deeply populated in there

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:24):

Dune had at first a few limitations like rules can only output over one directory, etc... that was due the way the incremental domain were setup, devs are slowly lifting these limitations

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:24):

I have a dune file in src which I want to add a rule for coqchk to

view this post on Zulip Ali Caglayan (Nov 15 2021 at 15:25):

(rule (alias validate)
  (deps (glob_files *.vo))
  (action (run coqchk -R . LogiCoq %{deps} -o))
)

works but checks a lot of stdlib too

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:26):

See _build/log

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:26):

but indeed I guess that's specific to coqchk?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:26):

also a single rule per .vo may be better

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:27):

if you don't update all the .vo's at once

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:27):

I am busy this week, but if someone would like to add (validate) to (coq.theory) I'd happy to help

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:27):

in fact, we don't even need to add validate, just generate the rules

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:27):

so people can do dune build @dir/coqchk

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:28):

or whatever we want to call that, I don't think setting up the rules is so expensive

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:30):

yeah just update the core rule for .vo in coq_rules.ml , and add a rule to call coqchk, with an alias as a way to trigger it

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:31):

aliases play the role of virtual targets, so they are used for the cases that a rule produces no targets, like tests indeed

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2021 at 15:31):

if you produce a target then no need to use an alias, you can always trigger the rule by the target

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 15:38):

without -norec (fixed), calls to coqchk are IIRC virtually constant-time, so per-file rules don’t seem so convenient in that mode…

view this post on Zulip Karl Palmskog (Nov 15 2021 at 15:40):

but just to be clear, if you don't pass -norec, then every time dependencies change, you have to recheck all of Stdlib that you use, even with Gaëtan's Dune rule, right?

view this post on Zulip Paolo Giarrusso (Nov 15 2021 at 15:50):

indeed. And -norec is harder to use than I thought: it takes a module name and does not seem to accept wildcards, so “no stdlib” or “only this project” seems hard to express?


Last updated: Jan 30 2023 at 17:03 UTC