Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[configure] Allow to avoid embedding the date on Coq's binaries #13858

Closed
wants to merge 1 commit into from

Conversation

ejgallego
Copy link
Member

This is quite important in some contexts, for example when using a
global compilation cache (as we do in Dune).

@ejgallego ejgallego added the part: build The build system. label Feb 13, 2021
@ejgallego ejgallego added this to the 8.14+rc1 milestone Feb 13, 2021
@ejgallego ejgallego requested a review from a team as a code owner February 13, 2021 23:05
@ejgallego ejgallego requested a review from a team February 13, 2021 23:05
@ejgallego ejgallego requested a review from a team as a code owner February 13, 2021 23:05
configure.ml Outdated Show resolved Hide resolved
sysinit/usage.ml Outdated
Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
Coq_config.version (Option.default "n/d" Coq_config.date);
Printf.printf "compiled on %s with OCaml %s\n"
(Option.default "n/d" Coq_config.compile_date) Coq_config.caml_version
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we print nothing instead of on n/d?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was wondering about this, as what could case less breakage to tools possibly parsing this etc...

I think I do prefer to print something, for example the default for many users of dune-build-info is to print

version: n/a

when the version is not available, so I dunno, I still have a small preference for printing "n/a"

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

n/d or n/a?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've changed it to n/a which is more correct.

This is quite important in some contexts, for example when using a
global compilation cache (as we do in Dune).
@silene
Copy link
Contributor

silene commented Feb 14, 2021

Let us not bother with -embed-date. Just remove those dates altogether.

If only date was the actual release date, as documented, it could make sense to keep it, but that is just a lie.

Coq is currently classified as "unreproducible build" by Debian. Let us take advantage of this pull request to make a step toward improving the situation.

@Zimmi48
Copy link
Member

Zimmi48 commented Feb 14, 2021

Removing this date would also be useful to Nix, where currently the date shown is a constant like "Jan 1st, 1970" / "1980".

@ejgallego
Copy link
Member Author

ejgallego commented Feb 14, 2021

Let us not bother with -embed-date. Just remove those dates altogether.

If only date was the actual release date, as documented, it could make sense to keep it, but that is just a lie.

Indeed that could make sense, but IMHO should go to a separate PR as it will modify the released packages causing potentially some breakage if people is parsing some of the outputs, this PR has the good property that it changes nothing for release builds.

Coq is currently classified as "unreproducible build" by Debian. Let us take advantage of this pull request to make a step toward improving the situation.

Unfortunately we'd still have #11229 which seems tricky to solve. Regarding configure IMHO it is easy for Debian to patch it so they get a constant date.

@silene
Copy link
Contributor

silene commented Feb 16, 2021

IMHO should go to a separate PR

See #13863 for a counter-proposal.

@gares
Copy link
Member

gares commented Feb 16, 2021

See #13863 for a counter-proposal.

It looks much simpler to me.

Copy link
Member

@gares gares left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IMO embedding the date is so useless that it does not deserve a config flag. The other approach seems just fine.

@SkySkimmer
Copy link
Contributor

+1 for #13863

@SkySkimmer SkySkimmer added the needs: decision Awaiting for a decision by the devs. label Feb 17, 2021
@ejgallego
Copy link
Member Author

Ok, closing this in favor of the full removal.

@ejgallego ejgallego closed this Feb 17, 2021
@coqbot-app coqbot-app bot removed this from the 8.14+rc1 milestone Feb 17, 2021
@ejgallego ejgallego deleted the configure+embed_date branch February 17, 2021 15:02
@ejgallego ejgallego added this to Done in Dune Mar 6, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
needs: decision Awaiting for a decision by the devs. part: build The build system.
Projects
Dune
  
Done
Development

Successfully merging this pull request may close these issues.

None yet

5 participants