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.

Sign up for GitHub

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

Jump to bottom

Coq makefile: provide variables to extend the flags passed to coq, coqchk, coqdoc #7025

Merged
merged 4 commits into from
Mar 23, 2018
Merged

Coq makefile: provide variables to extend the flags passed to coq, coqchk, coqdoc #7025

merged 4 commits into from
Mar 23, 2018

Conversation

RalfJung
Copy link
Contributor

@RalfJung RalfJung commented Mar 20, 2018 •
edited by gares

This provides a way to pass extra flags to coq/coqchk/coqdoc without overwriting the default flags.

Fix #6659

@RalfJung RalfJung mentioned this pull request Mar 20, 2018
Closed
@gares
Copy link
Member

gares commented Mar 21, 2018

The contents of the current doc can be seen here:
https://coq.inria.fr/distrib/current/refman/tools.html#Makefile
there is a section containing the variables you are allowed to set in the .local file.
I think there should be another section listing the variables one can pass on the command line, and that list should include the variables of this PR + TIME* (explained in the current doc) + VERBOSE.

coq_makefile's doc is in the process of being migrated to sphinx:
https://github.com/coq/coq/projects/16#card-8049587
so I think we should de-correlate this PR from the doc format (you write the new doc in the first comment of this PR, I later take care of making a PR out of it) when @maximedenes has ported chapter 15 to sphinx.

@gares gares added this to To Review in Enrico's work ) via automation Mar 21, 2018
@gares gares added the needs: documentation Documentation was not added or updated. label Mar 21, 2018
@gares gares self-assigned this Mar 21, 2018
@gares gares added this to the 8.9+alpha1 milestone Mar 21, 2018
@Zimmi48 Zimmi48 added the kind: feature New user-facing feature request or implementation. label Mar 21, 2018
@RalfJung
Copy link
Contributor Author

so I think we should de-correlate this PR from the doc format (you write the new doc in the first comment of this PR, I later take care of making a PR out of it) when @maximedenes has ported chapter 15 to sphinx.

Just to be sure I understand: You are saying that this PR (#7025) should not have doc changes, and you will ping me later (post-sphinxing) about adding these two variables to the doc?

@RalfJung
Copy link
Contributor Author

The VST Ci timed out, it seems? Can someone restart it?

@gares
Copy link
Member

gares commented Mar 21, 2018

I was asking you to write the doc here, as a comment, and then I would do the job of making a PR out of it on the .rst file @maximedenes will produce.

VST is timing out everywhere, ignore it this time.

@RalfJung
Copy link
Contributor Author

Like so?

@gares
Copy link
Member

gares commented Mar 22, 2018

Well, I was not clear, I meant a "comment on github", not "a commit containing a comment", but that is fine too (I just wanted the text).

@RalfJung
Copy link
Contributor Author

Oh. Sorry for that^^

@gares gares removed the needs: documentation Documentation was not added or updated. label Mar 22, 2018
@gares gares moved this from Review to Merge in Enrico's work ) Mar 22, 2018
@gares
Copy link
Member

gares commented Mar 22, 2018

@RalfJung I'll probably add a line to CHANGES and push the commit to your branch (this seems to be the protocol, including this "heads up" message)

@gares gares added the needs: changelog entry This should be documented in doc/changelog. label Mar 22, 2018
@gares gares removed the needs: changelog entry This should be documented in doc/changelog. label Mar 23, 2018
@gares gares merged commit 3a929e9 into coq:master Mar 23, 2018
Enrico's work ) automation moved this from Merge to Done Mar 23, 2018
gares added a commit that referenced this pull request Mar 23, 2018
@gares
Merge PR #7025: Coq makefile: provide variables to extend the flags p…
22e4ffa 
…assed to coq, coqchk, coqdoc
@RalfJung
Copy link
Contributor Author

Thanks :)

maximedenes
maximedenes reviewed Mar 23, 2018
View reviewed changes
CHANGES
@@ -1,3 +1,11 @@
Changes from 8.8.2 to 8.9+beta1
Copy link
Member

Choose a reason for hiding this comment

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

@gares what is Coq 8.8.2 ?

Copy link
Member

Choose a reason for hiding this comment

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

I suppose this is expecting two minor releases like that was done for Coq 8.7. We used to write "Changes beyond 8.8" instead which wasn't putting any expectation.

@Zimmi48 Zimmi48 modified the milestones: 8.9+alpha1, 8.9 Mar 31, 2018
@JasonGross JasonGross mentioned this pull request Apr 15, 2018
Closed
@JasonGross
Copy link
Member

This broke a part of the fiat-crypto build not tested by the CI (not tested due to the printing bug). What's a good way to get my hands on the correct flags to pass to coqc (when I -include Makefile.coq), that works with both 8.8 and master?

@SkySkimmer SkySkimmer mentioned this pull request Apr 15, 2018
Closed
@SkySkimmer
Copy link
Contributor

(cc from fiat-crypto issue)
I think if you just add $(COQLIBS) to the command it will be OK, repeating -R/-Q/-I doesn't seem to cause errors.

@RalfJung
Copy link
Contributor Author

Oh, so you have custom extension in Makefile.coq.local or so that use these variables? Yeah for these cases, this is a breaking change... I did not realize that. Should we still proceed?

JasonGross added a commit to JasonGross/coq that referenced this pull request Apr 20, 2018
@JasonGross
[ci] Also make some display targets for fiat-crypto
e81e281 
This will catch things like
coq#7025 (comment)
@JasonGross JasonGross mentioned this pull request Apr 20, 2018
Merged
Zimmi48 pushed a commit to Zimmi48/coq that referenced this pull request Apr 23, 2018
@JasonGross @Zimmi48
[ci] Also make some display targets for fiat-crypto
4c47a8e 
This will catch things like
coq#7025 (comment)

(cherry picked from commit e81e281)
@RalfJung RalfJung deleted the coq_makefile branch May 7, 2018 12:09
@gares gares mentioned this pull request May 11, 2018
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maximedenes maximedenes maximedenes left review comments

@Zimmi48 Zimmi48 Zimmi48 left review comments

@gares gares gares approved these changes

@silene silene Awaiting requested review from silene

Assignees

@gares gares

Labels
kind: feature New user-facing feature request or implementation.
Projects
No open projects
Enrico's work )
  
Done (
Milestone
8.9+beta1
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@RalfJung @gares @JasonGross @SkySkimmer @maximedenes @Zimmi48