Add support for CoqMakefile.local-late #12411

JasonGross · 2020-05-25T23:18:20Z

This allows users to write rules that depend on variables such as
VOFILES and VDFILE, which is essential in some of my use-cases (for
example, to properly handle seamless version switching, I need to make
all of the .vo files depend on a file where I record the version of Coq
being used).

Fixes #10912

Kind: feature / infrastructure.

Added / updated test-suite
Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

Does this qualify for 8.12 / 8.12+beta1?

Zimmi48 · 2020-05-26T10:37:12Z

Does this qualify for 8.12 / 8.12+beta1?

Nope, sorry.

SkySkimmer · 2020-05-26T10:41:57Z

Test suite change is incorrect according to CI

gares · 2020-05-26T14:35:36Z

Can't you just move down the inclusion of Makefile.coq.local.
I see this strategy is more backward compatible, but I may at least give it a try.

JasonGross · 2020-05-26T16:20:37Z

Can't you just move down the inclusion of

Oh, yeah, if there was no reason to have it be so early in the first place (e.g., overriding variables before the rest of the file processes them), then, yeah, let's just move it to the bottom of the file

JasonGross · 2020-06-24T16:59:05Z

Sorry for the late reply, I'm looking into this again now.

Note that moving it downwards breaks the use-case of overriding CAMLFLAGS (or OCAMLLIBS or COQSRCLIBS) and expecting CAMLDOCFLAGS to automatically pick up this change. We can either accept this cost, or I can replace all uses of $(CAMLFLAGS) with $(CAMLFLAGS) $(OCAMLWARN) and then change the := setting of CAMLDOCFLAGS to a =. What do you think should be done here?

As per coq#12411 (comment), instead of using a local-late file, we just move the local file down. This means that we need to replace all the relevant := assignments with = so that users can still override variables, and this mandates that we split up CAMLFLAGS.

JasonGross · 2020-06-24T17:11:47Z

Okay, I've changed the := to =. I believe this is ready for review again.

JasonGross · 2020-06-24T21:21:42Z

@gares It seems that just moving the local file to the bottom breaks many of the variable overriding features, e.g., how Mtac2 overrides COQ_SRC_SUBDIRS. It's possible that by changing all the variable assignments from := to =, we could fix this, but I'm quite hesitant to rely on nuances in when make evaluates which variables. I'm inclined to stick with the simpler solution of having both files.

As per coq#12411 (comment), instead of using a local-late file, we just move the local file down. This means that we need to replace all the relevant := assignments with = so that users can still override variables, and this mandates that we split up CAMLFLAGS.

This reverts commit 8715429. It actually breaks uses of variable overriding in the wild, as per coq#12411 (comment)

As per coq#12411 (comment), instead of using a local-late file, we just move the local file down. This means that we need to replace all the relevant := assignments with = so that users can still override variables, and this mandates that we split up CAMLFLAGS.

This reverts commit 8715429. It actually breaks uses of variable overriding in the wild, as per coq#12411 (comment)

gares · 2020-06-25T08:54:55Z

The variables one can override are documented. I don't recall that one to be documented as overrideable, and should not become so since it reflects Coq sources layout. Mtac2 should be fixed, IMO we should report a bug. Did you investigate the other failures?

gares · 2020-06-25T12:35:22Z

CC @Janno @beta-ziliani : do you recall why you had to override that makefile variable?

Janno · 2020-06-25T12:44:51Z

CC @Janno @beta-ziliani : do you recall why you had to override that makefile variable?

It was introduced when porting to 8.8 in 677df93. We previously had
-I $(COQMF_COQLIB)/user-contrib/Unicoq as an alternative but I guess that broke with 8.8.

Then for a short while we didn't have COQ_SRC_SUBDIRS (Mtac2/Mtac2#127) but that broke Coq's windows builds so now we have it again.

JasonGross · 2020-06-25T17:17:27Z

Did you investigate the other failures?

I did not, let me push another build so I can see the failures

doc/sphinx/practical-tools/utilities.rst

JasonGross · 2020-06-27T17:05:14Z

It seems that Mtac2 is the only failure. Regarding the Mtac2 failure, I found:

I'm much afraid that using $(shell ocamlfind printconf destdir) as a destination install seems broken and this is what broke the windows build.

As this is a coq_makefile project, you should integrate with where coq_makefile thinks the plugins should be going. For example, this patch will try to install in my root ~/.opam folder even if called with a coq_makefile coming from a ./configure -local Coq.

The problem is indeed not easy as coq_makefile lacks the proper integration with OCamlbuild to make this work. But given this approach seems broken I'd suggest to revert and instead move to a different build system if you need ocamlfind integration.

Originally posted by @ejgallego in unicoq/unicoq#17 (comment)

So indeed the issue here seems to be that coq_makefile doesn't have good enough support for this use case, which @vbgl describes in unicoq/unicoq#17:

To give some more context and motivation, I’d like to be able to install Unicoq and then use it as any third-party library. For instance, here is a patch to Mtac2 that shows that Unicoq can be used without hard-coding the path where it is installed nor repeating esoteric commands like “Declare ML Module "unicoq".”.

What should be done?

As per coq#12411 (comment)

jfehrle

The doc looks good. Nonetheless, a few more suggestions--I leave it up to you whether to include them.

doc/sphinx/practical-tools/utilities.rst

doc/changelog/08-tools/12411-makefile-local-late.rst

doc/sphinx/practical-tools/utilities.rst

tools/CoqMakefile.in

gares · 2021-04-27T13:56:25Z

doc/sphinx/practical-tools/utilities.rst

+The optional file ``CoqMakefile.local-late`` is included at the end of the generated
+file ``CoqMakefile``.  The following is a partial list of accessible variables:
+
+:COQ_VERSION:


This variable is also available in the non -late file (I'm using it already). Please move it upward.
Ditto for COQMAKEFILE_VERSION, COQC and COQFLAGS and COQLIBS.

I did not check the others.

All variables are available for use in recipes of rules in the non-late file, as well as in the definitions of variables assigned using =. They are also available in the prerequisites of rules only if you double the $ and enable secondary expansion. However, these variables are not available when naming the outputs of rules, nor in top-level ifeq/ifneq statements, nor in variables assigned with :=. (I presume your use-cases involve the former kind and not the latter kind?) Do you have suggestions for making this distinction more clear in the documentation?

Indeed. I think it is fine, your explanation could also go in the doc, since the external pointer is a bit boring to follow.

I've added some explanation in the doc, please take a look

gares

please move the non -late specific variable doc to the previous section

As per coq#12411 (comment)

JasonGross · 2021-05-12T14:42:37Z

Rebased. Is this ready for merge?

gares · 2021-05-15T07:09:18Z

The test suite is broken

As per coq#12411 (comment)

JasonGross · 2021-05-15T16:04:02Z

No idea why the behavior changed, but I've updated the expected output.

As requested in PR comments Change passive voice to active voice and fix a grammar error As per coq#12411 (comment) Add more documentation about Makefile var use Also apply suggestions from code review Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

This allows users to write rules that depend on variables such as VOFILES and VDFILE, which is essential in some of my use-cases (for example, to properly handle seamless version switching, I need to make all of the .vo files depend on a file where I record the version of Coq being used). Fixes coq#10912

No idea why the make output is different on MacOS and nix (see https://dev.azure.com/coq/coq/_build/results?buildId=10659&view=logs&jobId=a5e52b91-c83f-5429-4a68-c246fc63a4f7&j=a5e52b91-c83f-5429-4a68-c246fc63a4f7&t=bde16fc7-7659-5b1c-12aa-0110866d993c or see https://github.com/coq/coq/pull/12411/checks?check_run_id=808290881) but this should fix the discrepency.

As requested in PR comments Change passive voice to active voice and fix a grammar error As per coq#12411 (comment) Add more documentation about Makefile var use Also apply suggestions from code review Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

JasonGross · 2021-05-27T22:43:25Z

CI Green, @gares I think this is finally ready for merge

gares · 2021-05-27T23:43:37Z

@coqbot merge now

JasonGross added kind: infrastructure CI, build tools, development tools. part: tools Coqdoc, coq_makefile, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels May 25, 2020

JasonGross requested review from a team as code owners May 25, 2020 23:18

Zimmi48 added this to the 8.13+beta1 milestone May 26, 2020

SkySkimmer added the needs: fixing The proposed code change is broken. label May 26, 2020

JasonGross force-pushed the makefile-local-late branch from ce75697 to 0b4735e Compare June 24, 2020 17:11

JasonGross removed the needs: fixing The proposed code change is broken. label Jun 24, 2020

JasonGross added a commit to JasonGross/coq that referenced this pull request Jun 24, 2020

Revert "[coq_makefile] Move down local, no local-late"

6e75aee

This reverts commit 8715429. It actually breaks uses of variable overriding in the wild, as per coq#12411 (comment)

JasonGross force-pushed the makefile-local-late branch from 0b4735e to 6e75aee Compare June 24, 2020 21:23

JasonGross added a commit to JasonGross/coq that referenced this pull request Jun 24, 2020

Revert "[coq_makefile] Move down local, no local-late"

0e8b591

This reverts commit 8715429. It actually breaks uses of variable overriding in the wild, as per coq#12411 (comment)

JasonGross force-pushed the makefile-local-late branch from 6e75aee to 0e8b591 Compare June 24, 2020 21:25

JasonGross commented Jun 27, 2020

View reviewed changes

doc/sphinx/practical-tools/utilities.rst Outdated Show resolved Hide resolved

SkySkimmer added the needs: fixing The proposed code change is broken. label Jul 1, 2020

JasonGross added a commit to JasonGross/coq that referenced this pull request Apr 26, 2021

Change passive voice to active voice and fix a grammar error

3d1290e

As per coq#12411 (comment)

JasonGross requested a review from jfehrle April 26, 2021 12:54

jfehrle approved these changes Apr 26, 2021

View reviewed changes

gares reviewed Apr 27, 2021

View reviewed changes

gares requested changes Apr 27, 2021

View reviewed changes

gares approved these changes Apr 30, 2021

View reviewed changes

JasonGross added a commit to JasonGross/coq that referenced this pull request Apr 30, 2021

Change passive voice to active voice and fix a grammar error

879b33e

As per coq#12411 (comment)

JasonGross force-pushed the makefile-local-late branch 2 times, most recently from d1de27a to d04da97 Compare April 30, 2021 15:43

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 4, 2021

JasonGross added a commit to JasonGross/coq that referenced this pull request May 12, 2021

Change passive voice to active voice and fix a grammar error

4907da0

As per coq#12411 (comment)

JasonGross force-pushed the makefile-local-late branch from 2d55ea7 to aae16b9 Compare May 12, 2021 14:42

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 12, 2021

JasonGross added a commit to JasonGross/coq that referenced this pull request May 15, 2021

Change passive voice to active voice and fix a grammar error

4aed1a4

As per coq#12411 (comment)

JasonGross force-pushed the makefile-local-late branch from aae16b9 to dbe94db Compare May 15, 2021 16:03

JasonGross force-pushed the makefile-local-late branch from dbe94db to c6992cc Compare May 15, 2021 16:05

JasonGross force-pushed the makefile-local-late branch from c6992cc to 03c5055 Compare May 26, 2021 21:00

JasonGross and others added 3 commits May 27, 2021 11:56

JasonGross force-pushed the makefile-local-late branch from 03c5055 to 04c4af2 Compare May 27, 2021 15:56

coqbot-app bot merged commit b7d10ab into coq:master May 27, 2021

JasonGross deleted the makefile-local-late branch May 28, 2021 00:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for CoqMakefile.local-late #12411

Add support for CoqMakefile.local-late #12411

JasonGross commented May 25, 2020

Zimmi48 commented May 26, 2020

SkySkimmer commented May 26, 2020

gares commented May 26, 2020

JasonGross commented May 26, 2020

JasonGross commented Jun 24, 2020 •

edited

JasonGross commented Jun 24, 2020

JasonGross commented Jun 24, 2020

gares commented Jun 25, 2020 •

edited

gares commented Jun 25, 2020

Janno commented Jun 25, 2020

JasonGross commented Jun 25, 2020

JasonGross commented Jun 27, 2020

jfehrle left a comment

gares Apr 27, 2021 •

edited

JasonGross Apr 28, 2021

gares Apr 30, 2021

JasonGross Apr 30, 2021

gares left a comment

JasonGross commented May 12, 2021

gares commented May 15, 2021

JasonGross commented May 15, 2021

JasonGross commented May 27, 2021

gares commented May 27, 2021

Add support for CoqMakefile.local-late #12411

Add support for CoqMakefile.local-late #12411

Conversation

JasonGross commented May 25, 2020

Zimmi48 commented May 26, 2020

SkySkimmer commented May 26, 2020

gares commented May 26, 2020

JasonGross commented May 26, 2020

JasonGross commented Jun 24, 2020 • edited

JasonGross commented Jun 24, 2020

JasonGross commented Jun 24, 2020

gares commented Jun 25, 2020 • edited

gares commented Jun 25, 2020

Janno commented Jun 25, 2020

JasonGross commented Jun 25, 2020

JasonGross commented Jun 27, 2020

jfehrle left a comment

Choose a reason for hiding this comment

gares Apr 27, 2021 • edited

Choose a reason for hiding this comment

JasonGross Apr 28, 2021

Choose a reason for hiding this comment

gares Apr 30, 2021

Choose a reason for hiding this comment

JasonGross Apr 30, 2021

Choose a reason for hiding this comment

gares left a comment

Choose a reason for hiding this comment

JasonGross commented May 12, 2021

gares commented May 15, 2021

JasonGross commented May 15, 2021

JasonGross commented May 27, 2021

gares commented May 27, 2021

JasonGross commented Jun 24, 2020 •

edited

gares commented Jun 25, 2020 •

edited

gares Apr 27, 2021 •

edited