Stream: Coq devs & plugin devs

Topic: How to get `revision` file to update on build


view this post on Zulip Ali Caglayan (Feb 07 2022 at 15:49):

How can I get the revision file to update on each build? Dune doesn't seem to care about updating it.

view this post on Zulip Gaëtan Gilbert (Feb 07 2022 at 15:50):

there's no PHONY in dune afaik

view this post on Zulip Ali Caglayan (Feb 07 2022 at 15:51):

Can I get coq-core.boot to depend on it somehow?

view this post on Zulip Ali Caglayan (Feb 07 2022 at 15:51):

I'm confused how I could do that

view this post on Zulip Gaëtan Gilbert (Feb 07 2022 at 15:52):

maybe if you hack dune
otherwise I doubt it

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 19:15):

@Ali Caglayan have you look into the dune build info thing?

view this post on Zulip Ali Caglayan (Feb 07 2022 at 19:18):

How does that work?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 19:18):

it is built in support to get the revision from git

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 19:18):

I think there is doc

view this post on Zulip Ali Caglayan (Feb 07 2022 at 19:33):

Hmm it just printed "dev"

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:24):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:24):

There was an old issue where we discussed that

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 21:24):

using git-describe

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 23:54):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 23:54):

Actually there are many different specs for this kind of information

view this post on Zulip Emilio Jesús Gallego Arias (Feb 07 2022 at 23:54):

then we can implement it

view this post on Zulip Ali Caglayan (Feb 08 2022 at 09:50):

Have a look at this PR I m as de yesterday

view this post on Zulip Ali Caglayan (Feb 08 2022 at 09:50):

I made

view this post on Zulip Ali Caglayan (Feb 08 2022 at 09:50):

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 09:51):

Here I am calling git at configure time

view this post on Zulip Ali Caglayan (Feb 08 2022 at 09:51):

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 09:51):

But this obviously doesn't work without git being present

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 10:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 10:05):

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

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

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 15:08):

That way the revision file keeps updated

view this post on Zulip Ali Caglayan (Feb 08 2022 at 15:11):

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 15:11):

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

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

view this post on Zulip Guillaume Melquiond (Feb 08 2022 at 15:24):

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 15:30):

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

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 15:33):

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

view this post on Zulip Ali Caglayan (Feb 08 2022 at 15:33):

Perhaps it is not a good idea in the end

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

that would print the info for bug reports

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

so you just tell users to run that

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:20):

dune-build-info works well for a most users

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 16:20):

that install packages using managerss

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Feb 08 2022 at 18:31):

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

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:07):

but hash-based is pretty hard to beat actually

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:08):

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

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:08):

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 01:15):

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

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

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