Stream: Coq devs & plugin devs

Topic: Pass flags to coqc

Maxime Dénès (Mar 18 2022 at 15:58):

I want to pass a -foo flag to coqc, for building stdlib, test-suite and CI. What should I do?

Ali Caglayan (Mar 18 2022 at 15:59):

For stdlib you need to pass it in theories/dune

Ali Caglayan (Mar 18 2022 at 16:00):

For test-suite it is a bit harder

Maxime Dénès (Mar 18 2022 at 16:00):

lol

Ali Caglayan (Mar 18 2022 at 16:00):

For individual files you can pass a flag by putting a header

Gaëtan Gilbert (Mar 18 2022 at 16:01):

for CI just fake it (change the default in coqargs)

Ali Caglayan (Mar 18 2022 at 16:01):

But to change all files, you will need to change it manually in the test-suite makefile

Gaëtan Gilbert (Mar 18 2022 at 16:01):

Gaëtan Gilbert said:

for CI just fake it (change the default in coqargs)

this also works for stdlib/test suite

Maxime Dénès (Mar 18 2022 at 16:01):

What I really want in the end is to be able to launch CI with and without the flags

Maxime Dénès (Mar 18 2022 at 16:01):

Like two targets

Gaëtan Gilbert (Mar 18 2022 at 16:02):

CI projects are free to run coqc directly so the only solution is to modify coqc

Ali Caglayan (Mar 18 2022 at 16:02):

Just always have the option on for now :)

Gaëtan Gilbert (Mar 18 2022 at 16:02):

you can make it controlled by an env var

Maxime Dénès (Mar 18 2022 at 16:02):

Sorry, I mean: run the test-suite with and without the flags, in our CI

Ali Caglayan (Mar 18 2022 at 16:03):

The test-suite job in the pipeline you mean?

Ali Caglayan (Mar 18 2022 at 16:03):

<s>There is no simple way to change all the flags</s>

Gaëtan Gilbert (Mar 18 2022 at 16:03):

for passing flags in the test suite see what test-suite:base+async does

Maxime Dénès (Mar 18 2022 at 16:03):

Yes, ideally I want to make to copies of that job in my branch

Maxime Dénès (Mar 18 2022 at 16:03):

One with the flag one without

Maxime Dénès (Mar 18 2022 at 16:04):

Thanks for the suggestion, my need is very much like async indeed

Gaëtan Gilbert (Mar 18 2022 at 16:05):

(for stdlib see the base+async job)

Enrico Tassi (Mar 18 2022 at 16:35):

Oh, but does this means that CI builds the stdlib not using dune? Makefile.build strikes back?

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:38):

Yes, the pr for getting rid of makefile.build is not yet finished

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:39):

we will get to it next week I think

Enrico Tassi (Mar 18 2022 at 16:39):

when we move to just dune, what will be the right way to pass coqc an option? I did suggest @Maxime Dénès to use a dune profile and have (profile foo (coq (flags -my-option))) but apparently this option is not passed while building the prelude.

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:40):

Ali and I are pushing some changes to coqdep that will make the job easier

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:40):

Enrico Tassi said:

when we move to just dune, what will be the right way to pass coqc an option? I did suggest Maxime Dénès to use a dune profile and have (profile foo (coq (flags -my-option))) but apparently this option is not passed while building the prelude.

I need to think about that but as we will use gen_rules I guess that a config for gen_rules will do

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:41):

profile should also work in recent versions, but we wont use that as we will control rules locally

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:41):

if that doens't work that's a bug

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:41):

flags should be passed for prelude too

Enrico Tassi (Mar 18 2022 at 16:42):

That is the PR https://github.com/ocaml/dune/pull/3547

Gaëtan Gilbert (Mar 18 2022 at 16:42):

Enrico Tassi said:

Oh, but does this means that CI builds the stdlib not using dune? Makefile.build strikes back?

depends on the job

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:42):

Enrico Tassi said:

That is the PR https://github.com/ocaml/dune/pull/3547

I know that PR, that PR was buggy actually see current test suite

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:43):

and https://github.com/ocaml/dune/pull/4758

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:44):

Gaëtan Gilbert said:

Enrico Tassi said:

Oh, but does this means that CI builds the stdlib not using dune? Makefile.build strikes back?

depends on the job

hopefully soon it won't

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:44):

we are making progress on getting gen_rules ready

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:45):

we actually removed the coqdep printing + parsing, and now we also share the context so it is quite fast

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:45):

next week I have some time so hopefully we can finish it

Enrico Tassi (Mar 18 2022 at 16:45):

Ah, then setting dune lang to 2.9 would have made it work for Maxime?

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:46):

@Enrico Tassi not sure if we versioned the fix, maybe you can write the problem in the dune channel or bug tracker?

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:46):

Dune 2.9 has the fix

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

Yes, I confirm I didn't version the fix

Enrico Tassi (Mar 18 2022 at 16:47):

Maxime told me he has 2.9.1

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

so coq flags in profile are broken for 2.8 and less

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

I'd need to see if there is some bug remaining

Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

post a reproduction case in the dune stream

Maxime Dénès (Mar 18 2022 at 17:39):

So the "funny" part is I lost a significant part of my day trying to do it with Dune just because I didn't know the configure + make workflow was still there. I knew the COQUSERFLAGS env var.

Maxime Dénès (Mar 18 2022 at 18:15):

Am I missing something or does dune build treat stdlib warnings as non fatal?

Maxime Dénès (Mar 18 2022 at 18:15):

I mean warning emitted by Coq, this time

Théo Zimmermann (Mar 18 2022 at 18:17):

Last time I checked, this was still the case.

Maxime Dénès (Mar 18 2022 at 18:18):

What was still the case? From what I see dune build does not fail when stdlib emits a warning.

Maxime Dénès (Mar 18 2022 at 18:18):

(to test it, you can just add Set Foobar. in a file)

Maxime Dénès (Mar 18 2022 at 18:19):

The developer profile for make does treat them as fatal.

Théo Zimmermann (Mar 18 2022 at 18:21):

Still the case that Dune does not treat coqc warnings as fatal.

Maxime Dénès (Mar 18 2022 at 18:21):

I see. But why is that?

Théo Zimmermann (Mar 18 2022 at 18:21):

Despite a bug report already being opened on the topic I think.

Maxime Dénès (Mar 18 2022 at 18:21):

Incidentally, this made me completely mis-evaluate the state of my branch in parsing mode. I had a lot of debug output, so didn't see the warnings. And I was convinced they were treated as errors, like they used to be with make.

Gaëtan Gilbert (Mar 18 2022 at 18:26):

https://github.com/coq/coq/pull/14241

Emilio Jesús Gallego Arias (Mar 18 2022 at 19:28):

Yes the current state is not the best, we need to finish the gen_rules PR ASAP

Emilio Jesús Gallego Arias (Mar 18 2022 at 19:30):

The current dune build method for vo files has a few drawbacks, exactly what was discussed on the call. Once we re-introduce gen_rules we should close all the regressions afaict

Emilio Jesús Gallego Arias (Mar 18 2022 at 19:33):

Moreover we will need developer feedback on the PR porting the test-suite to dune. The PR brings many improvements but user experience is quite different so need help

Maxime Dénès (Mar 20 2022 at 18:38):

I switched back to make, to be able to pass the -only-parsing flag

Maxime Dénès (Mar 20 2022 at 18:38):

but it is almost unusable

Maxime Dénès (Mar 20 2022 at 18:38):

it is extremely slow (> 1s per binary/plugin to produce, probably because it makes a full call to dune each time)

Maxime Dénès (Mar 20 2022 at 18:38):

when I do make clean, I need to redo ./configure

Maxime Dénès (Mar 20 2022 at 18:40):

when I replace ./configure -profile devel to what ./configure -help says it is equivalent to, it changes the behavior

Maxime Dénès (Mar 20 2022 at 18:41):

when I replay coqc invocations as shown by make VERBOSE=1 it fails with findlib errors

Maxime Dénès (Mar 20 2022 at 18:41):

so for now, I have no concrete solution to get a workable dev setup that allows me to pass flags to coqc

Maxime Dénès (Mar 20 2022 at 19:01):

do we have an ETA for the fixes?

Maxime Dénès (Mar 20 2022 at 19:02):

(the point is to schedule my activity, not to put pressure)

Théo Zimmermann (Mar 20 2022 at 19:25):

Maxime Dénès said:

when I replace ./configure -profile devel to what ./configure -help says it is equivalent to, it changes the behavior

Indeed, this doc is outdated. Now this profile does more.

Maxime Dénès (Mar 20 2022 at 19:43):

I had severely underestimated the situation with the build system. For better efficiency, I will reschedule the activity on this patch to after these regressions are fixed.

Last updated: Sep 15 2024 at 13:02 UTC