Stream: Coq devs & plugin devs

Topic: Pass flags to coqc


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

view this post on Zulip Ali Caglayan (Mar 18 2022 at 15:59):

For stdlib you need to pass it in theories/dune

view this post on Zulip Ali Caglayan (Mar 18 2022 at 16:00):

For test-suite it is a bit harder

view this post on Zulip Maxime Dénès (Mar 18 2022 at 16:00):

lol

view this post on Zulip Ali Caglayan (Mar 18 2022 at 16:00):

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

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 16:01):

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

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

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

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 16:01):

Like two targets

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

view this post on Zulip Ali Caglayan (Mar 18 2022 at 16:02):

Just always have the option on for now :)

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 16:02):

you can make it controlled by an env var

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

view this post on Zulip Ali Caglayan (Mar 18 2022 at 16:03):

The test-suite job in the pipeline you mean?

view this post on Zulip Ali Caglayan (Mar 18 2022 at 16:03):

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

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 16:03):

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 16:03):

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 16:03):

One with the flag one without

view this post on Zulip Maxime Dénès (Mar 18 2022 at 16:04):

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

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 16:05):

(for stdlib see the base+async job)

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:38):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:39):

we will get to it next week I think

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:41):

if that doens't work that's a bug

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:41):

flags should be passed for prelude too

view this post on Zulip Enrico Tassi (Mar 18 2022 at 16:42):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:43):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:44):

we are making progress on getting gen_rules ready

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:45):

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

view this post on Zulip Enrico Tassi (Mar 18 2022 at 16:45):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:46):

Dune 2.9 has the fix

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

Yes, I confirm I didn't version the fix

view this post on Zulip Enrico Tassi (Mar 18 2022 at 16:47):

Maxime told me he has 2.9.1

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

so coq flags in profile are broken for 2.8 and less

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 16:47):

post a reproduction case in the dune stream

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 18:15):

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 18:15):

I mean warning emitted by Coq, this time

view this post on Zulip Théo Zimmermann (Mar 18 2022 at 18:17):

Last time I checked, this was still the case.

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 18:18):

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 18:19):

The developer profile for make does treat them as fatal.

view this post on Zulip Théo Zimmermann (Mar 18 2022 at 18:21):

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

view this post on Zulip Maxime Dénès (Mar 18 2022 at 18:21):

I see. But why is that?

view this post on Zulip Théo Zimmermann (Mar 18 2022 at 18:21):

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

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

view this post on Zulip Gaëtan Gilbert (Mar 18 2022 at 18:26):

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

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

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

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

view this post on Zulip Maxime Dénès (Mar 20 2022 at 18:38):

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

view this post on Zulip Maxime Dénès (Mar 20 2022 at 18:38):

but it is almost unusable

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

view this post on Zulip Maxime Dénès (Mar 20 2022 at 18:38):

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

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

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

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

view this post on Zulip Maxime Dénès (Mar 20 2022 at 19:01):

do we have an ETA for the fixes?

view this post on Zulip Maxime Dénès (Mar 20 2022 at 19:02):

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

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

view this post on Zulip 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: Feb 06 2023 at 19:03 UTC