How can I get the revision
file to update on each build? Dune doesn't seem to care about updating it.
there's no PHONY in dune afaik
Can I get coq-core.boot to depend on it somehow?
I'm confused how I could do that
maybe if you hack dune
otherwise I doubt it
@Ali Caglayan have you look into the dune build info thing?
How does that work?
it is built in support to get the revision from git
I think there is doc
Hmm it just printed "dev"
Indeed I think it only prints the version if you install the files? I don't recall the details. But it is easy to make a rule, that depends on .git and outputs revision
There was an old issue where we discussed that
using git-describe
But this won't work for nix right, since it needs to be reproducible. Implicitly relying on git makes that difficult.
Umm, maybe we can describe what we want exactly first?
Actually there are many different specs for this kind of information
then we can implement it
Have a look at this PR I m as de yesterday
I made
https://github.com/coq/coq/pull/15639
Here I am calling git at configure time
In fact I like this better than the revision file since that can get stale
But this obviously doesn't work without git being present
I will have a look but not before Fri sorry, actually we could just discuss in the WG
it is a bit tricky as imagine a documentation-only commit
You don't want to rebuild any ML or VO files!
Emilio Jesús Gallego Arias said:
it is a bit tricky as imagine a documentation-only commit
or commit message amend
OK, then it seems checking hash in ocaml won't be a good idea. Would it be possible to set up a git hook to update revision on commits/HEAD change?
That way the revision file keeps updated
But in the end I don't know how to go forward with this really
I need to learn about reproducible builds and what others do some more
What is your motivation for embedding the checksum inside Coq? Reproducible builds are always performed from the outside, never from the inside. In other words, it is the outside environment that tells how the software will be built, not the software that tells in which environment it was originally built.
(Archetypal examples are requirements.txt
in Python, package-lock.json
in Javascript, and so on.)
When people report bugs on master it is useful to include the commit hash.
I have seen in other development versions of software a commit hash being printed so I always thought it was standard practice
But the more I try to implement it the more I realize what can go wrong
Perhaps it is not a good idea in the end
If I remeber the last discussions about it on the dune part, the idea is to have something "softer" that works on most cases, but if not, just prints dev
but in a way that you don't break for example incremental builds, etc...
we could do like Debian and have a coq_reportbug.sh script
that would print the info for bug reports
so you just tell users to run that
and that can call git, see if the tree is dirty, etc...
dune-build-info works well for a most users
that install packages using managerss
if we call git after compilation how can we tell the user didn't reset in the meantime?
If a user is running master, then he is also able to run git describe IMO when he reports a bug. Newcomers should not use master (nor compile coq by hand)
usually coq_reportbug.sh will do a few checks by hand, if the bug is coming from master etc...
If you really care, you could include the tree git hash instead of the commit git hash.
But that’s harder to use, so I do think rebuilding one file and relinking is the correct reaction to “git commit —amend”
It’d be nice if it just rebuilt a file with let git_hash = “cafebabe0123”
.
Either way, including an hash works even if you install your development coq, and later find a bug.
not allowed to relink, that leads to rebuilding the stdlib
if you find a bug in a random dev version but can't reproduce on a released version or new master, just forget about it
If you’re really opposed to commit messages making a difference, the git tree hash only hashes the tree content and gives no information about the history; the downside is that looking up the commit for a tree requires scanning all commits
@Gaëtan Gilbert would that rebuild the stdlib even with SOURCE_DATE_EPOCH set? You want that for reproducible builds
what does the date have to do with anything? you're putting a different hash in the coqc binary, so dependency analysis says all the stdlib depends on something that has changed since you last built it even though you just updated some git metadata
oh right, you’re talking of dune
’s dependency analysis. I was thinking about Coq producing actually different binaries…
I suspect a smarter dependency analysis might work, but it’s not worth just for this. It’d worth to support in dune if you want to ignore, say, changes to Qed
bodies.
I think dune devs would be happy to implement a smarter deps analysis, if someone would specify it
but hash-based is pretty hard to beat actually
when you consider all the things you need to support including distributed builds
there are various forms of "smart hashing" one can do with knowledge of language semantics
for example, you could hash the file that is actually parsed by Coq, as opposed to lexed
That could be an interesting feature to add to the low-level build engine
tho the amount of engineering work it would require for sure would make it justifiable just for this
It is pretty easy just to output revision and have coqc look for it
I know they sometimes hash .class
files in Java instead of source, one idea we had was to use the SerAPI sexps as the .class
. But overhead obviously large. Would be better to tap directly into AST, and make sure one is independent of locs.
In Scala they actually hash interfaces, and since a few years they track dependencies at the method level. So that if you change one method's signature, clients not depending on it will not get recompiled.
@Paolo Giarrusso I fully agree that doing that for Coq does make sense
but we need finer granularity than what a file-based system can provide IMHO
In retrospect, it’s a bit surprising that has acceptable overhead, but the alternative (Scalac/Dotty) is super-slow (also compared to Javac)
Last updated: May 31 2023 at 15:01 UTC