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?
what's the status of native compute on dune?
Requires 2.9 and explicit enable
also there seem to be still some bug in the split boot build, not very annoying for dev use
I will release 2.9.2 to fix it, some silly flag problem it seems
By dev workflow I mean "non-install workflow"
we can still test the install targets as we do now
we just nuke -profile devel
in dev mode I think we rarely want to build native, at least not by default
see PR https://github.com/coq/coq/pull/12974
oh something I didn't merge yet is coqnative support
I can merge the first part, but the true split setup needs more thinking
That's PR https://github.com/pulls?q=is%3Aopen+is%3Apr+author%3Aejgallego+archived%3Afalse+native
I dunno, would we have kept the coq_dune
approach, it would be long time we would be done
maybe we should just resurrect it
and get rid of the makefiles
WDYT?
Dune 3.0 will properly support that so no more voboot
yeah let's do that
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
except for native I think we're pretty close to removing Makefile.make
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
was a bad idea to go this path [insight is 20/20]
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
Gaëtan Gilbert said:
except for native I think we're pretty close to removing Makefile.make
although there's also the doc
doc is IMHO a minor thing
minor in what sense?
Minor in terms of fixing I hope.
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).
Gaëtan Gilbert said:
minor in what sense?
In terms of make burden, also Dune 3.0 does support our doc worflow finally!
@Théo Zimmermann IIANM Dune 3.0 has everything we need, Rudi did implement the install part too
So unless something weird happens we can have the coq-doc opam package
Oh, he did! That's great to hear!
We should probably try ASAP to check that it fits all our needs before Dune 3.0 is released.
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
.
That's an interesting feature!
Tho you can implement it today without a lot of burden
well, I'm not sure what you mean to diff dirs
if you have like a new and old dir, you can just output the list of files and use the regular diff
action
Yes I'm planning to check
that the directory stuff works fine, tho dune also uses sphinx so we'll try it to eat its own soup
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?
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.
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.
I see what you mean, that's supported by the engine, not sure if there is a way to express in on the language
if you specify the files in the rules that is "parallel", unless there is a dependency
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).
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.
I need someone to volunteer to shepherd such change before I start work tho
Similar for the dune + test_suite PR
I'm afraid that after thinking a bit about it, the feedback I get is too vague
like "oh we want everything to keep working"
where each person has a different definition of "everything" and "working"
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?
Hi @Théo Zimmermann , the idea is to have a way to build .vo files that is controlled by Coq devs
as of today, the dune build rules are implemented in the tool, so that has proven to be inconvenient
the original implementation using coq_dune for Coq was more flexible
as we can control the rules
downsides were the lack of support for dynamic dependencies in the rule language, but this has been lifted in 3.0
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
that supports compositions of theories, etc...
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)))
and that is controlled by Coq devs
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
there are some minor technical details, but IMHO nothing important
externally, all users do observe the same built layout and interface
so we rid of the cumbersome compat layer
which has proven to be too painful IMHO
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?
It doesn't require Dune 3.0 , what dune 3.0 provides is the ability to avoid a bootstrap process
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
calling configure before the build , until 3.0 is assumed
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...
coq_dune is hardcoded to the stdlib
developers should use the built-in rules in dune IMHO
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
technically configure was like that too
you can capture that with a simple make rule tho
still better than the current setup
which does exactly that
Emilio Jesús Gallego Arias said:
technically configure was like that too
?
for example if you renamed a plugin directory
I have hit this case and got me crazy
have make coq-dune
regen the dune file if some file changed
still rarer than adding or removing a Require somewhere
still unsound , less frequent but unsound if you handle by hand, as we used to do
[dune rule for configure captures that]
coq_dune used to be not too bad as we called coqdep only once
I don't claim that's perfect, I claim that's much better than the current setup
a single make rule
theories/dune: $(vfiles)
coq_dune ...
which can go away soonish
yes indeed
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
now we have (subdir foo (rules ....))
so that's much better
ok I think that could work
yeah not perfect but still better than the mess the bridge is
and build_vo goes away
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
I guess we could do
ifndef DUNE_MORE_THAN_THREE
theories/dune: ...
endif
too
yes
good idea indeed!
not sure how we get the static dune files to be compatible with all situations though
(non coq_dune, coq_dune with dune 2, coq_dune with dune 3)
We need to pick a default
I guess we should do the default the built-in for now
we need some trick for git, I think that's all
Last updated: Oct 13 2024 at 01:02 UTC