Stream: Coq devs & plugin devs

Topic: Deprecating legacy dev workflow


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

Gaëtan Gilbert said:

main problem is we test that the legacy build can build, install and that the installed result can be used
but we don't test the non-install dev workflow

Indeed, what we do here, maybe we should deprecate legacy dev workflow?

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

what's the status of native compute on dune?

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

Requires 2.9 and explicit enable

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

also there seem to be still some bug in the split boot build, not very annoying for dev use

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

I will release 2.9.2 to fix it, some silly flag problem it seems

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

By dev workflow I mean "non-install workflow"

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

we can still test the install targets as we do now

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

we just nuke -profile devel

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

in dev mode I think we rarely want to build native, at least not by default

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

see PR https://github.com/coq/coq/pull/12974

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

oh something I didn't merge yet is coqnative support

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

I can merge the first part, but the true split setup needs more thinking

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

That's PR https://github.com/pulls?q=is%3Aopen+is%3Apr+author%3Aejgallego+archived%3Afalse+native

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

I dunno, would we have kept the coq_dune approach, it would be long time we would be done

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

maybe we should just resurrect it

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

and get rid of the makefiles

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

WDYT?

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

Dune 3.0 will properly support that so no more voboot

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

yeah let's do that

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

Emilio Jesús Gallego Arias said:

in dev mode I think we rarely want to build native, at least not by default

sure, but we should still have an ok dev workflow for native devs

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

except for native I think we're pretty close to removing Makefile.make

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

Gaëtan Gilbert said:

except for native I think we're pretty close to removing Makefile.make

Let's discuss tomorrow but I think we can get rid of it this week

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

was a bad idea to go this path [insight is 20/20]

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

compared to the mess we have, having to do voboot for the "legacy" build seems very minor, and that'll go away in Dune 3.0 anywyas

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

Gaëtan Gilbert said:

except for native I think we're pretty close to removing Makefile.make

although there's also the doc

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

doc is IMHO a minor thing

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

minor in what sense?

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 12:40):

Minor in terms of fixing I hope.

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 12:41):

But my opinion on the doc build is that until some support that will likely not even arrive in Dune 3.0 for installing directory targets, we should revert to a makefile (and nuke the Dune rules entirely).

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

Gaëtan Gilbert said:

minor in what sense?

In terms of make burden, also Dune 3.0 does support our doc worflow finally!

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

@Théo Zimmermann IIANM Dune 3.0 has everything we need, Rudi did implement the install part too

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

So unless something weird happens we can have the coq-doc opam package

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:17):

Oh, he did! That's great to hear!

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:19):

We should probably try ASAP to check that it fits all our needs before Dune 3.0 is released.

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:19):

Is it possible to diff on entire directories as well? That would be useful to extend the check-gram rules to handle the rst files like in the legacy Makefile.doc.

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

That's an interesting feature!

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

Tho you can implement it today without a lot of burden

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

well, I'm not sure what you mean to diff dirs

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

if you have like a new and old dir, you can just output the list of files and use the regular diff action

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

Yes I'm planning to check

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

that the directory stuff works fine, tho dune also uses sphinx so we'll try it to eat its own soup

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:21):

if you have like a new and old dir, you can just output the list of files and use the regular diff action

Can you do the file listing dynamically?

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:23):

Another slight annoyance of calling the diff action on each relevant file is that if one fails, you need to promote and re-run to get the next failure, and you may need to repeat this as many times as there are changed files.

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:24):

So it would be great if it was possible to say to Dune to do the diff "in parallel" on a list of files (e.g., with a .new pattern for new files) and promote everything at once.

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

I see what you mean, that's supported by the engine, not sure if there is a way to express in on the language

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

if you specify the files in the rules that is "parallel", unless there is a dependency

view this post on Zulip Théo Zimmermann (Nov 09 2021 at 13:36):

OK, interesting! My experience was with fullGrammar and orderedGrammar. In this case, there is a dependency, so it is not parallel. But that's good to know that for the rst files, diffing / promoting can be done in parallel (this means that the burden can be reduced to diffing / promoting three times, and maybe we can be clever and reduce that to only once).

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

As discussed on the call, we could improve things a lot using coq_dune and removing the makefiles for all .vo files, the workflow would be almost identical, with the only difference of who generates the files.

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

I need someone to volunteer to shepherd such change before I start work tho

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

Similar for the dune + test_suite PR

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

I'm afraid that after thinking a bit about it, the feedback I get is too vague

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

like "oh we want everything to keep working"

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

where each person has a different definition of "everything" and "working"

view this post on Zulip Théo Zimmermann (Nov 10 2021 at 18:49):

Sorry I wasn't able to be on the Call today. Would the approach of reintroducing coq_dune be only for the "legacy" build? Or is the goal to get rid of it entirely?

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

Hi @Théo Zimmermann , the idea is to have a way to build .vo files that is controlled by Coq devs

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

as of today, the dune build rules are implemented in the tool, so that has proven to be inconvenient

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

the original implementation using coq_dune for Coq was more flexible

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

as we can control the rules

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

downsides were the lack of support for dynamic dependencies in the rule language, but this has been lifted in 3.0

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

so the way I see is that we would still have two build paths, one where theories/dune is the current one, and uses dune built-in rules

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

that supports compositions of theories, etc...

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

the other is where we generate theories/dune to be a set of (rule (target foo.vo) (deps ... foo.v) (action (run coqc foo.v)))

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

and that is controlled by Coq devs

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

eventually both approaches should unify, but this setup has a very big advantage, and it is that all .vo files are controlled by dune, as opposed as the current setup

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

there are some minor technical details, but IMHO nothing important

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

externally, all users do observe the same built layout and interface

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

so we rid of the cumbersome compat layer

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

which has proven to be too painful IMHO

view this post on Zulip Théo Zimmermann (Nov 11 2021 at 15:39):

So this means that the setup where theories/dune is generated would require Dune 3.0 and would be more powerful (being able to handle native, vos and whatever we need) while the one which would use the Coq rules in Dune would have the advantage of only requiring Dune 2.5?

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

It doesn't require Dune 3.0 , what dune 3.0 provides is the ability to avoid a bootstrap process

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

which is convenient, but IMHO not a big deal, we can live IMHO fine for those willing to have our local version of the rules

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

calling configure before the build , until 3.0 is assumed

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

the main difference is that the one "native" to dune, it is of course a bit faster, and also allows for the composition features etc...

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

coq_dune is hardcoded to the stdlib

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

developers should use the built-in rules in dune IMHO

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

Emilio Jesús Gallego Arias said:

calling configure before the build , until 3.0 is assumed

it needs to run when dependencies change, that's not configure

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

technically configure was like that too

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

you can capture that with a simple make rule tho

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

still better than the current setup

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

which does exactly that

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

Emilio Jesús Gallego Arias said:

technically configure was like that too

?

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

for example if you renamed a plugin directory

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

I have hit this case and got me crazy

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

have make coq-dune regen the dune file if some file changed

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

still rarer than adding or removing a Require somewhere

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

still unsound , less frequent but unsound if you handle by hand, as we used to do

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

[dune rule for configure captures that]

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

coq_dune used to be not too bad as we called coqdep only once

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

I don't claim that's perfect, I claim that's much better than the current setup

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

a single make rule

theories/dune: $(vfiles)
    coq_dune ...

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

which can go away soonish

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

yes indeed

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

before we had trouble doing this as a rule as we had to generate a dune file for each subdir, that was a pain to handle in make

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

now we have (subdir foo (rules ....)) so that's much better

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 16:00):

ok I think that could work

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

yeah not perfect but still better than the mess the bridge is

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

and build_vo goes away

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

how to select will still be a bit hacky, until we move to 3.0, then in this case we can use an env_var or whatever

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 16:01):

I guess we could do

ifndef DUNE_MORE_THAN_THREE
theories/dune: ...
endif

too

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

yes

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

good idea indeed!

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 16:03):

not sure how we get the static dune files to be compatible with all situations though

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 16:04):

(non coq_dune, coq_dune with dune 2, coq_dune with dune 3)

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

We need to pick a default

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

I guess we should do the default the built-in for now

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

we need some trick for git, I think that's all


Last updated: Feb 01 2023 at 16:03 UTC