Centralise and improve documentation on Coq #5755
Conversation
|
Yes, this was discussed before. Note that the original Coq mode for Dune followed this approach, but the section on Coq was later removed by a refactoring of the manual. I think there's consensus on backtracking on that one and doing as you propose. |
|
@jfehrle I agree that the Coq documentation for the use of dune needs to be improved also. We are currently working on improving dune support for Coq so that it becomes a viable alternative to coq_makefile. There are still a few rungs in the carpet that need to be flattened out. |
|
Note you are undoing 920667d Posting for reference. |
|
@ejgallego Not quite. There the documentation was in the "advanced topics" file. Now we have a dedicated file. |
|
@christinerose Thanks! |
Alizter
force-pushed
the
coq-doc
branch
2 times, most recently
from
0db8264 to
9c4c09b
Compare
|
@ejgallego Can you try out my mini plugin tutorial, I think I may have botched it. |
doc/coq.rst
Outdated
| scope (i.e. under the same :ref:`dune-project` domain). This restriction will | ||
| be lifted in the future. Note that composition with the Coq standard library | ||
| is supported, but in this case the ``Coq`` prefix has been made available in a | ||
| qualified way, since Coq lang 0.2. |
There was a problem hiding this comment.
That already is a reason to fix https://github.com/coq/coq/issues/16091 soon
Alizter
force-pushed
the
coq-doc
branch
3 times, most recently
from
f0cfc8e to
d28bc15
Compare
There was a problem hiding this comment.
Some suggestions. Use what's helpful. While this is an improvement, I think it's still not going to be easy for Coq users to make sense of. The Coq documentation should have a section explaining how to create the dune files.
Do take a look at coq/coq#15888. Let's make sure that it and dune are conceptually consistent. We can also create a follow-on Coq doc PR with similar info on dune.
|
@jfehrle Let me reply to a few of your points here so that they don't become lost.
I don't have any particular opinion about the "theory" terminology. I believe it is intended in the loosest sense to be a collection of .v files. Perhaps a more suitable term would have been Coq library. However this would be quite confusing in Dune, since an unqualified "library" exclusively refers to an OCaml library. Therefore, I see some of the motivation with this nomenclature.
As of today, Dune is not able to build projects on which your Coq theory may depend on. The theories field of the coq.theory stanza may only refer to other theories defined by a coq.theory rule. Today, there are limitations to this. For instance, those theories must be inside the same dune-project. If you require fiat-crypto in your Coq project, and fiat-crypto is globally installed (as usual in a user-contrib folder), then Dune does not know about it, nor will it attempt to rebuild it, when you build your theory. Today, Coq is able to find the user-contrib folder itself, without any help from Dune. Aside from the fact that fiat-crypto is not a Dune project, if we were to build it using Dune, and were expecting Dune to build the I'll say a bit more about what Dune can and intends to do in a bit.
I would say that composition is the ability for Dune libraries to find other libraries in a rigid and reliable manner. In order to fully appreciate what we intend by composition let us describe some internal notions. A scope is where Dune will go searching for dependencies and targets. These are:
Today, Dune is able to "compose" within all 3 scopes when building OCaml libraries. For Coq, Dune is only currently able to do the first. This means you can have a single dune-project file, with multiple coq.theory stanzas within scope (in subdirectories etc.). Inter-project scope composition allows you to "plop" a dune-project, inside of another. In OCaml, say I have a library about keeping track of my groceries. It may turn out that I need a good way to display my grocery list. I can therefore find a library about pretty printing strings that I would like to depend on. I would not have to install this library, I simply have to drop the sources (which have their own dune-project file) into my project directory (with my dune-project file). Now when I refer to the string library in my OCaml stanzas, Dune will know how to find the library, and how to build only the parts it needs since that library is also a dune project. This is what we mean by composition. The same for Coq is not yet implemented. In fact, it is very close to being finished in my PR with Rudi here: #5784 What this would mean, is that fiat-crypto, if it were a dune project, would simply have to include the sources of This sort of composition doesn't only have to be in a dune-project however. There is something called a dune-workspace. When included in a directory where all the subdirectories are dune-projects, it can act like a large project file. You can imagine being able to develop multiple repositories simultaneously, whilst allowing them to depend on each other. Finally I would like to say a bit about the third scope of installed libraries. Today, when you build a Dune Coq project which depends on an external library, this will only work "by accident" if Coq itself is able to find that library in the loadpath. Since Dune has no idea about the external library, this means it cannot give informative error messages, or deem that things need to be rebuilt since the installed sources have changed. This is where Rudi, Emilio and I have been discussing having a notion of "installed" library. For OCaml, Dune is able to depend installed OCaml libraries with the properties I described before. It is a future implementation detail, for us to do something similar for Coq. Hopefully this clears it up a bit. I am more than happy to answer any more questions. |
|
Indeed @jfehrle , I chose to introduce "theory" for a Coq library as otherwise it would have become quite confusing as Dune already uses heavily "library" for OCaml libs. |
|
@jfehrle good point about composition, I am not sure how the manual is today, but last time I looked "composition of libraries" was used in Dune manual but it was not explained anywhere! If that's still the case, it needs to be fixed, otherwise Coq can just link to where composition is defined. |
|
@jfehrle Thanks for the review! |
|
If you want me to proofread it again after these changes, please let me know! |
|
@christinerose I told @ejgallego to merge this a bit later, but I wouldn't mind another read through. Even if this gets merged before, I can always submit another PR fixing anything you caught. :-) |
|
I'll wait for @christinerose pass |
There was a problem hiding this comment.
A few further comments.
@Alizter I appreciate your lengthy explanations here in the PR, but it would be so much better if you could (eventually) get their substance into the dune or Coq doc.
After you're done with this PR, we should talk and consider what I said in coq/coq#15888
| Coq Language Version 1.0 | ||
| ~~~~~~~~~~~~~~~~~~~~~~~~ |
There was a problem hiding this comment.
| Coq Language Version 1.0 | |
| ~~~~~~~~~~~~~~~~~~~~~~~~ | |
| Coq Language Version 1.0 (planned) | |
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
Is 1.0 planned or experimental/under development? i.e., will dune accept "1.0" as the language version today?
The challenges in describing functionality that's not yet complete are a) it may still change, so you need an extra pass on the doc and b) users may misread the doc and expect the future items already work.
There was a problem hiding this comment.
This is the end result of all the planned features. I would be more comfortable omitting all mentions of 1.0 since it is very confusing. @ejgallego what do you think?
| Notice the ``theories`` field in ``B`` allows one :ref:`coq-theory` to depend on | ||
| another. Another thing to note is the inclusion of the :ref:`include_subdirs` |
There was a problem hiding this comment.
How do users identify the dependencies and update their dune files? Will there be tooling to do that automatically? I'm not sure how significant an issue this may be for users.
There was a problem hiding this comment.
That's a bit of an art, and likely Dune won't be able to help a lot until 2.0 coq lang.
There was a problem hiding this comment.
I thought it would be an update to coqdep. Indeed, it might be cool if dune could read and apply coqdep output. IIUC.
There was a problem hiding this comment.
Oh, I misunderstood you. Dune of course calls coqdep to find dependencies of .v files, (theories ...) is for dependency on theories, that is to say, to put in scope whole set of compiled files into a prefix, that is to say, -Q.
Now, dune can't help a lot the user to know where a particular module is in terms of theories/packages.
There was a problem hiding this comment.
I hope to do some modifications to Coq itself in the future. Perhaps by adding another mode. So that it doesn't find libraries unless it has been provided in the command line. This would mean that dune has to provide all the dependencies, therefore we can be more sure if there are any missing deps.
There was a problem hiding this comment.
The idea is to enhance coqdoc so it can tell you what top-level modules/packages it depends on--the bits that need to appear in -Q options. It could look at _CoqProject files and/or in the Coq loadpath. (handwaving here)
| Dune supports running a Coq toplevel binary such as ``coqtop``, which is | ||
| typically used by editors such as CoqIDE or Proof General to interact with Coq. |
There was a problem hiding this comment.
| Dune supports running a Coq toplevel binary such as ``coqtop``, which is | |
| typically used by editors such as CoqIDE or Proof General to interact with Coq. | |
| Dune supports running Coq binaries such as ``coqtop`` from the build tree, which is | |
| typically used by editors such as CoqIDE or Proof General to interact with Coq. |
Few people use coqtop as a tool. Perhaps "coqide" is a better example?
There was a problem hiding this comment.
This one requires some explanation since it is a little confusing otherwise. @rlepigre added a command called dune coq top to dune earlier this year. The intention was to get PG to interface with dune. As you might know, PG does not use coqidetop but rather a separate mode on coqtop directly. This command allows calling coqtop on a file, and rebuilding what is necessary. AFAIK it is working well for users using emacs/PG.
This isn't to say that the command name isn't confusing however. I hope that in the future, we can also support coqidetop using this command, which would allow for some editor integration with dune. I don't think this command is intended for use by regular users, rather just a technical backend for PG for the time being.
The command grouping is a little strange, but make sense from the point of view of dune. Subcommands define the scope of functionality of a program, so there was a choice between dune coqtop and dune coq top. The latter allows for more coq related commands to be included under this group. I have no plans for any coq commands in dune however, nor am I aware of any more.
There was a problem hiding this comment.
I hope that in the future, we can also support coqidetop using this command
AFAIU, this is already supported with the --toplevel option.
There was a problem hiding this comment.
@Zimmi48 It doesn't work unfortunately, though I am not sure what is wrong.
There was a problem hiding this comment.
@Zimmi48 It doesn't work unfortunately, though I am not sure what is wrong.
That is surprising, what have you tried?
My understanding is that coqtop and coqidetop are kind of compatible in terms of the command-line arguments they expect, so I would have expected dune coq top --toplevel coqidetop some/file.v to do the trick.
There was a problem hiding this comment.
Is the problem the one showcased in #5552 ?
We need to fix that one asap.
There was a problem hiding this comment.
I don't remember if it was related to that. I will need to test further.
Alizter
force-pushed
the
coq-doc
branch
2 times, most recently
from
20a46a2 to
79955ba
Compare
There was a problem hiding this comment.
Although I have some minor suggestions/corrections, I'm approving this so you don't have to wait on me to merge. 😄
The ones that are optional are noted, and there are a few questions like if you can wrap section headers in monospace. Also, it would be best to make coqtop or coq top consistent, unless they mean two different things, like coq top is used in the command dune coq top and coqtop is the name of the thing. If this is true, perhaps Coqtop? Just for clarification.
Otherwise, it looks great!
|
|
||
| .. _coq-theory: | ||
|
|
||
| coq.theory |
There was a problem hiding this comment.
| coq.theory | |
| ``coq.theory`` |
If this can be in monospace as a heading, it would be best to put it in monospace. If not, no worries!
There was a problem hiding this comment.
Doesn't look great unfortunately:
|
@christinerose Regarding They are two different things where the former is for invoking the latter in a special way. It is an unfortunate discrepancy in my opinion. |
Signed-off-by: Ali Caglayan <alizter@gmail.com>
|
No worries! As long as it's clear to the reader. |
|
Thanks everybody for the great feedback. We think it is time to checkpoint on this, additional PRs and issues about the Coq doc are most welcome! |
This is documenting things that will appear in coq/coq#5695 so that should be merged before.
We improve the documentation of Coq support in dune by centralizing all the scraps of documentation we had before and concentrating them in their own file. We enrich this information with various examples too.
cc @ejgallego @rgrinberg
and cc @Zimmi48 @jfehrle who are on the Coq documentation team.