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

documentation should be built with coq-native installed #14269

Open
gares opened this issue May 6, 2021 · 7 comments
Open

documentation should be built with coq-native installed #14269

gares opened this issue May 6, 2021 · 7 comments
Labels
kind: infrastructure CI, build tools, development tools.
Projects
User documentation Dune

Comments

@gares
Copy link
Member

gares commented May 6, 2021

Look at https://coq.github.io/doc/v8.13/refman/proof-engine/tactics.html#coq:tacv.native_cast_no_check
it says that native_compute if off...
@gares
Copy link
Member Author

gares commented May 6, 2021

CC @coq/doc-maintainers

@Zimmi48
Copy link
Member

Zimmi48 commented May 6, 2021

This is likely because the version we deploy is the one that is built with Dune.

@Zimmi48
Copy link
Member

Zimmi48 commented May 6, 2021

In particular, it has nothing to do with the coq-native package since we don't use opam to build the doc in the CI.

@Zimmi48 Zimmi48 added the kind: infrastructure CI, build tools, development tools. label May 6, 2021
@SkySkimmer
Copy link
Contributor

Maybe we should just disable that warning for the doc

@ejgallego
Copy link
Member

Now that we have coqnative in master I hope we can make this work with dune very soon [or we could already enable the support for "old style" native in dune, but that'd require bumping dune for that build to Dune 2.8)

@Zimmi48
Copy link
Member

Zimmi48 commented May 7, 2021

Maybe we should just disable that warning for the doc

Sounds like another reasonable solution and it could be implemented in the short-term.

@Zimmi48 Zimmi48 added this to Infrastructure in User documentation May 7, 2021
@ejgallego ejgallego mentioned this issue Jul 3, 2023
Merged
@ejgallego
Copy link
Member

I think nothing is blocking a fix for this?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: infrastructure CI, build tools, development tools.
Projects
Dune
  
Awaiting triage
User documentation
Status: Infrastructure
User documentation
  
Infrastructure
Milestone
No milestone
Development

No branches or pull requests
4 participants
@gares @Zimmi48 @SkySkimmer @ejgallego