How to get `revision` file to update on build · Coq devs & plugin devs

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

Emilio Jesús Gallego Arias (Feb 07 2022 at 21:24):

There was an old issue where we discussed that

Emilio Jesús Gallego Arias (Feb 07 2022 at 21:24):

using git-describe

Ali Caglayan (Feb 07 2022 at 22:54):

But this won't work for nix right, since it needs to be reproducible. Implicitly relying on git makes that difficult.

Emilio Jesús Gallego Arias (Feb 07 2022 at 23:54):

Umm, maybe we can describe what we want exactly first?

Emilio Jesús Gallego Arias (Feb 07 2022 at 23:54):

Actually there are many different specs for this kind of information

Emilio Jesús Gallego Arias (Feb 07 2022 at 23:54):

then we can implement it

Ali Caglayan (Feb 08 2022 at 09:50):

Have a look at this PR I m as de yesterday

Ali Caglayan (Feb 08 2022 at 09:50):

I made

Ali Caglayan (Feb 08 2022 at 09:50):

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

Ali Caglayan (Feb 08 2022 at 09:51):

Here I am calling git at configure time

Ali Caglayan (Feb 08 2022 at 09:51):

In fact I like this better than the revision file since that can get stale

Ali Caglayan (Feb 08 2022 at 09:51):

But this obviously doesn't work without git being present

Emilio Jesús Gallego Arias (Feb 08 2022 at 10:04):

I will have a look but not before Fri sorry, actually we could just discuss in the WG

Emilio Jesús Gallego Arias (Feb 08 2022 at 10:05):

it is a bit tricky as imagine a documentation-only commit

Emilio Jesús Gallego Arias (Feb 08 2022 at 10:05):

You don't want to rebuild any ML or VO files!

Gaëtan Gilbert (Feb 08 2022 at 10:05):

Emilio Jesús Gallego Arias said:

it is a bit tricky as imagine a documentation-only commit

or commit message amend

Ali Caglayan (Feb 08 2022 at 15:08):

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?

Ali Caglayan (Feb 08 2022 at 15:08):

That way the revision file keeps updated

Ali Caglayan (Feb 08 2022 at 15:11):

But in the end I don't know how to go forward with this really

Ali Caglayan (Feb 08 2022 at 15:11):

I need to learn about reproducible builds and what others do some more

Guillaume Melquiond (Feb 08 2022 at 15:21):

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.

Guillaume Melquiond (Feb 08 2022 at 15:24):

(Archetypal examples are requirements.txt in Python, package-lock.json in Javascript, and so on.)

Ali Caglayan (Feb 08 2022 at 15:30):

When people report bugs on master it is useful to include the commit hash.

Ali Caglayan (Feb 08 2022 at 15:30):

I have seen in other development versions of software a commit hash being printed so I always thought it was standard practice

Ali Caglayan (Feb 08 2022 at 15:33):

But the more I try to implement it the more I realize what can go wrong

Ali Caglayan (Feb 08 2022 at 15:33):

Perhaps it is not a good idea in the end

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

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

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

but in a way that you don't break for example incremental builds, etc...

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

we could do like Debian and have a coq_reportbug.sh script

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

that would print the info for bug reports

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

so you just tell users to run that

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

and that can call git, see if the tree is dirty, etc...

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:20):

dune-build-info works well for a most users

Emilio Jesús Gallego Arias (Feb 08 2022 at 16:20):

that install packages using managerss

Gaëtan Gilbert (Feb 08 2022 at 16:22):

if we call git after compilation how can we tell the user didn't reset in the meantime?

Enrico Tassi (Feb 08 2022 at 16:24):

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)

Emilio Jesús Gallego Arias (Feb 08 2022 at 17:39):

usually coq_reportbug.sh will do a few checks by hand, if the bug is coming from master etc...

Paolo Giarrusso (Feb 08 2022 at 18:29):

If you really care, you could include the tree git hash instead of the commit git hash.

Paolo Giarrusso (Feb 08 2022 at 18:30):

But that’s harder to use, so I do think rebuilding one file and relinking is the correct reaction to “git commit —amend”

Paolo Giarrusso (Feb 08 2022 at 18:31):

It’d be nice if it just rebuilt a file with let git_hash = “cafebabe0123”.

Paolo Giarrusso (Feb 08 2022 at 18:32):

Either way, including an hash works even if you install your development coq, and later find a bug.

Gaëtan Gilbert (Feb 08 2022 at 18:34):

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

Paolo Giarrusso (Feb 08 2022 at 18:34):

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

Paolo Giarrusso (Feb 08 2022 at 18:35):

@Gaëtan Gilbert would that rebuild the stdlib even with SOURCE_DATE_EPOCH set? You want that for reproducible builds

Gaëtan Gilbert (Feb 08 2022 at 18:37):

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

Paolo Giarrusso (Feb 08 2022 at 18:43):

oh right, you’re talking of dune’s dependency analysis. I was thinking about Coq producing actually different binaries…

Paolo Giarrusso (Feb 08 2022 at 18:45):

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.

Emilio Jesús Gallego Arias (Feb 08 2022 at 21:07):

I think dune devs would be happy to implement a smarter deps analysis, if someone would specify it

Emilio Jesús Gallego Arias (Feb 08 2022 at 21:07):

but hash-based is pretty hard to beat actually

Emilio Jesús Gallego Arias (Feb 08 2022 at 21:08):

when you consider all the things you need to support including distributed builds

Karl Palmskog (Feb 08 2022 at 21:08):

there are various forms of "smart hashing" one can do with knowledge of language semantics

Karl Palmskog (Feb 08 2022 at 21:09):

for example, you could hash the file that is actually parsed by Coq, as opposed to lexed

Emilio Jesús Gallego Arias (Feb 08 2022 at 21:09):

That could be an interesting feature to add to the low-level build engine

Emilio Jesús Gallego Arias (Feb 08 2022 at 21:10):

tho the amount of engineering work it would require for sure would make it justifiable just for this

Emilio Jesús Gallego Arias (Feb 08 2022 at 21:10):

It is pretty easy just to output revision and have coqc look for it

Karl Palmskog (Feb 08 2022 at 21:15):

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.

Paolo Giarrusso (Feb 08 2022 at 22:30):

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.

Emilio Jesús Gallego Arias (Feb 09 2022 at 01:15):

@Paolo Giarrusso I fully agree that doing that for Coq does make sense

Emilio Jesús Gallego Arias (Feb 09 2022 at 01:15):

but we need finer granularity than what a file-based system can provide IMHO

Paolo Giarrusso (Feb 09 2022 at 06:07):

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