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

[build] [doc] Build a few more targets hygienically #14212

Merged
merged 1 commit into from
May 4, 2021
Merged

[build] [doc] Build a few more targets hygienically #14212

merged 1 commit into from
May 4, 2021

Conversation

ejgallego
Copy link
Member

This will help avoid problems with dirty tress in the future, and
should overall provide a better experience in terms of hygienic
builds.

@ejgallego ejgallego requested review from a team as code owners April 29, 2021 23:33
@Zimmi48 Zimmi48 added kind: infrastructure CI, build tools, development tools. part: build The build system. labels Apr 30, 2021
@Zimmi48 Zimmi48 added this to the 8.14+rc1 milestone Apr 30, 2021
@Zimmi48 Zimmi48 added the needs: fixing The proposed code change is broken. label Apr 30, 2021
@Zimmi48 Zimmi48 self-assigned this Apr 30, 2021
@Zimmi48
Copy link
Member

Zimmi48 commented Apr 30, 2021

Some stuff needs fixing:

Error: no rule to make target _build/default/doc/stdlib//Library.tex (or missing .PHONY)

BTW, why do we build this in the build:base job?

@Zimmi48 Zimmi48 mentioned this pull request Apr 30, 2021
Closed
@ejgallego
Copy link
Member Author

Fixing this now, sorry.

BTW, why do we build this in the build:base job?

This is a long story due indeed to problems with the build system , see #7515

@ejgallego
Copy link
Member Author

This is a long story due indeed to problems with the build system , see #7515

Concretely, the makefiles didn't support building the docs from the build:base artifact which is an installed Coq.

@ejgallego
Copy link
Member Author

Needs a bit more work due to the code using _build as output directory and dune cleaning targets it doesn't know about.

@ejgallego ejgallego marked this pull request as draft April 30, 2021 22:00
@Zimmi48
Copy link
Member

Zimmi48 commented May 1, 2021

Concretely, the makefiles didn't support building the docs from the build:base artifact which is an installed Coq.

OK. We should really fix that if we can. Otherwise, the coq-doc.opam package will never be fully functional. Also, I wanted to split the Nix package following the same schema (coq-core, coq-stdlib, coq-doc) but I will face the same problem.

@ejgallego ejgallego force-pushed the doc+out_of_tree_some_stuff branch 2 times, most recently from 97a6167 to ddf9c6a Compare May 1, 2021 14:11
@ejgallego
Copy link
Member Author

We should really fix that if we can.

We are not there yet, but some steps in this PR have been made so the doc build is relying on an install layout, I think we are close to actually doing that IMHO, as now Makefile.doc expects an installed Coq under either _build/install or build_vo

@ejgallego ejgallego force-pushed the doc+out_of_tree_some_stuff branch 3 times, most recently from 6323d7b to 194c01a Compare May 1, 2021 15:06
@ejgallego
[build] [doc] Build a few more targets hygienically
57b8408 
This will help avoid problems with dirty tress in the future, and
should overall provide a better experience in terms of hygienic
builds.

We also add a `doc-stdlib-html` target; fixes coq#14218
@ejgallego ejgallego force-pushed the doc+out_of_tree_some_stuff branch from 194c01a to 57b8408 Compare May 1, 2021 15:46
@ejgallego ejgallego marked this pull request as ready for review May 1, 2021 15:50
@ejgallego ejgallego requested a review from a team as a code owner May 1, 2021 15:50
@Zimmi48 Zimmi48 removed the needs: fixing The proposed code change is broken. label May 2, 2021
Zimmi48
Zimmi48 approved these changes May 3, 2021
View reviewed changes
Makefile.doc
@@ -133,8 +148,9 @@ doc/common/version.tex: config/Makefile

### Changelog

doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
$(DOC_BUILD_DIR)/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
Copy link
Member

Choose a reason for hiding this comment

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

What is the point of doing this out of tree if it is only used by the Sphinx build which is done in tree?

Copy link
Member Author

Choose a reason for hiding this comment

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

Indeed, I can defer this change to a possible sphinx out-of-tree PR; I did setup that in the hope of advancing a bit more on that front, but only did the stdlib part.

Copy link
Member

Choose a reason for hiding this comment

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

As you want. I can also merge as is.

Copy link
Member Author

Choose a reason for hiding this comment

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

Let's merge as-is if you want, and also tweak the rest of targets so we bulid the full doc hygienically too.

doc/dune
@@ -1,5 +1,7 @@
(rule
(targets unreleased.rst)
; We need to keep this as the sphinx build still requires this file
; in-tree, to be fixed hopefully soon
Copy link
Member

Choose a reason for hiding this comment

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

Actually, I think this is incorrect because when building the refman through Dune, the build is already done out of tree (Makefile.doc is not used in that case).

Copy link
Member Author

Choose a reason for hiding this comment

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

This is needed for the case you do a regular make build, then a dune build, otherwise dune will complain about the generated file; once we more the sphinx out of tree, this can be removed.

Copy link
Member

Choose a reason for hiding this comment

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

I see, thanks!

.gitlab-ci.yml
@@ -80,6 +80,7 @@ before_script:
- config/Makefile
- config/coq_config.py
- config/coq_config.ml
- config/dune.c_flags
Copy link
Member

Choose a reason for hiding this comment

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

When is this generated and what is this used for?

Copy link
Member Author

Choose a reason for hiding this comment

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

This is always generated by configure, it is used to setup the floating point flags for the kernel float vm machinery.

@Zimmi48
Copy link
Member

Zimmi48 commented May 4, 2021

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 079a721 into coq:master May 4, 2021
@ejgallego ejgallego deleted the doc+out_of_tree_some_stuff branch May 4, 2021 09:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 approved these changes

Assignees

@Zimmi48 Zimmi48

Labels
kind: infrastructure CI, build tools, development tools. part: build The build system.
Projects
None yet
Milestone
8.14+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@ejgallego @Zimmi48