Stream: Dune devs & users

Topic: dune rule for coqchk?

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?

Ali Caglayan (Nov 15 2021 at 14:43):

ping @Emilio Jesús Gallego Arias

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

Gaëtan Gilbert (Nov 15 2021 at 14:45):

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

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?

Paolo Giarrusso (Nov 15 2021 at 14:47):

You mean because by default dune builds everything?

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?

Karl Palmskog (Nov 15 2021 at 14:48):

but coq_makefile builds artifacts that are not built twice

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?

Gaëtan Gilbert (Nov 15 2021 at 14:49):

coqchk doesn't build artifacts

Paolo Giarrusso (Nov 15 2021 at 14:49):

Validate runs on the whole project both above and in coq_makefile

Paolo Giarrusso (Nov 15 2021 at 14:49):

But only when you call the appropriate target

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.

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

Gaëtan Gilbert (Nov 15 2021 at 14:52):

you can't trust a .ok file anyway

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.

Karl Palmskog (Nov 15 2021 at 14:52):

well, you can trust it if you generate it yourself

Paolo Giarrusso (Nov 15 2021 at 14:52):

(so the rerunning is not so frequent)

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?

Ali Caglayan (Nov 15 2021 at 15:11):

OK that seemed to work

Ali Caglayan (Nov 15 2021 at 15:11):

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

Ali Caglayan (Nov 15 2021 at 15:12):

Is there a better way to do this?

Ali Caglayan (Nov 15 2021 at 15:12):

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

Gaëtan Gilbert (Nov 15 2021 at 15:12):

vo files that come from src

glob_files src/*.vo?

Gaëtan Gilbert (Nov 15 2021 at 15:13):

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

Ali Caglayan (Nov 15 2021 at 15:13):

I have quite a few subdirectories

Gaëtan Gilbert (Nov 15 2021 at 15:14):

then you need quite a few globs

Emilio Jesús Gallego Arias (Nov 15 2021 at 15:15):

glob_files recurse but not sure if only in 3.0

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

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

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

Ali Caglayan (Nov 15 2021 at 15:20):

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

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

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

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

Ali Caglayan (Nov 15 2021 at 15:23):

OK let me start over then

Ali Caglayan (Nov 15 2021 at 15:23):

I have a src directory

Ali Caglayan (Nov 15 2021 at 15:23):

with multiple .v files deeply populated in there

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

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

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 15:26):

See _build/log

Emilio Jesús Gallego Arias (Nov 15 2021 at 15:26):

but indeed I guess that's specific to coqchk?

Emilio Jesús Gallego Arias (Nov 15 2021 at 15:26):

also a single rule per .vo may be better

Emilio Jesús Gallego Arias (Nov 15 2021 at 15:27):

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

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

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

Emilio Jesús Gallego Arias (Nov 15 2021 at 15:27):

so people can do dune build @dir/coqchk

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

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

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

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

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…

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?

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: Apr 16 2024 at 07:02 UTC