CoqIDE: Need a better way to load secondary modules

[jfehrle]

Fiat-crypto has a main package named Crypto and depends on another package named Rewriter. If I use these command-line settings to run CoqIDE, I can load ToFancyWithCasts.v and step through it in the debugger.

-R _build_ci/fiat_crypto/src Crypto
-R _build_ci/rewriter/src/Rewriter Rewriter
-I _build_ci/rewriter/src/Rewriter/Util/plugins

Without these lines, I get this failure:

Command line parameters are not very friendly. CoqIDE should have a better way to handle this case, such as putting them in a file akin to _CoqProject that the user could select from within CoqIDE. In effect there would be multiple _CoqProject files.

It would be helpful if the _CoqProject for fiat-crypto could specify this relationship. The challenge is that the pathname for Rewriter is system dependent. A comment noting the relationship would be a good development practice. I suppose we could try to define universal invariant package identifiers (e.g. the DNS name of the package's repository plus an optional pathname therein) and have each compiled package include that name. That's more complex.

Currently, when you open a source file in CoqIDE, it adds paths in its _CoqProject file to the loadpath for that buffer. Excerpt:

-R src Crypto   (* the only -R; there are no -Q *)
  :
src/Rewriter/Passes/ToFancyWithCasts.v

[ppedrot]

I really don't understand why you have to do this kind of manipulations. When I have to edit fiat-crypto, I just pass the _CoqProject file from its folder to CoqIDE. Any dependency is already available in the path because it has been installed in the user-contrib folder, so there is no need to do anything for those ones.

[Alizter]

For the record, @ppedrot is suggesting you do coqide -f _build_ci/fiat_crypto/_CoqProject. or which ever coqide instance you are calling.

[ppedrot]

This should even be automatic if your options are set correctly...

[Alizter]

I seem to recall it only working like that if I start coqide in _build_ci/fiat_crypto.

[jfehrle]

I really don't understand why you have to do this kind of manipulations. When I have to edit fiat-crypto, I just pass the _CoqProject file from its folder to CoqIDE. Any dependency is already available in the path because it has been installed in the user-contrib folder, so there is no need to do anything for those ones.

Neither Crypto nor Rewriter is an opam-installable package AFAIK. Nor is there any documentation about how to install packages in a non-opam installation of Coq. In particular, how does the logical name Crypto get added as the top directory for the package within user-contrib? The user has to create that directory manually?

Also, the extra src directory in fiat-crypto isn't part of the module name, so some rearrangement of directories would be required to make it work in user-contrib. Maybe fiat-crypto is a corner case. At the least the doc should mention the benefit of using something like -R . Bignums which avoids this problem.

Since the opam installation path includes the Coq version number, the user-contrib directory isn't a great place to keep your only git repository for your project. In that case, if you upgrade to a new version of Coq, you may wonder where your repository went. If it's on github then it's less of an issue.

[ppedrot]

In particular, how does the logical name Crypto get added as the top directory for the package within user-contrib?

It's the responsibility of the package to provide proper install scripts. In the case where there is an opam package, they install the relevant files in the Coq path so you don't have to do anything. If this doesn't work, it's a bug of the opam installer. But I suspect you're using a weird setup because I've never had this kind of issues with the fiat-crypto scripts. cc @JasonGross just in case.

At the least the doc should mention the benefit of using something like -R . Bignums which avoids this problem.

If you have to explicitly pass the path to bignums, you're definitely doing something very wrong. Once again, this folder should be living in your Coq installation.

Since the opam installation path includes the Coq version number, the user-contrib directory isn't a great place to keep your only git repository for your project.

Could you provide an overview of your setup? I am very confused.

[jfehrle]

@Alizter For the record, @ppedrot is suggesting you do coqide -f _build_ci/fiat_crypto/_CoqProject. or which ever coqide instance you are calling.

@ppedrot This should even be automatic if your options are set correctly...

@Alizter I seem to recall it only working like that if I start coqide in _build_ci/fiat_crypto.

When you edit a file, CoqIDE finds the associated _CoqProject and passes those options to coqidetop. That works fine when all the code is in a single package, but fiat-crypto relies on another package Rewriter that's not even structured to go into user-contrib since it has an extra src directory. Maybe fiat-crypto is very atypical in this regard.

[jfehrle]

At the least the doc should mention the benefit of using something like -R . Bignums which avoids this problem.

If you have to explicitly pass the path to bignums, you're definitely doing something very wrong. Once again, this folder should be living in your Coq installation.

This is only in the _CoqProject file for coq-bignums. I was not clear.

[jfehrle]

Since the opam installation path includes the Coq version number, the user-contrib directory isn't a great place to keep your only git repository for your project.

Could you provide an overview of your setup? I am very confused.

My regular setup is to run out of my Coq source tree. Separately, I'm looking at how a Coq platform installation is set up. In part, my goal is to understand the details well enough so that I can add something useful to the documentation (explanation of config behavior/concepts with some best practice suggestions).

[jfehrle]

In the case where there is an opam package, they install the relevant files in the Coq path so you don't have to do anything.

Are you sure fiat-crypto is an opam package? I don't find in the opam available packages list (if I'm looking at it correctly). How do you install it with opam or otherwise?

[SkySkimmer]

_build_ci doesn't use opam, why are you talking about opam?

[jfehrle]

As I said

My regular setup is to run out of my Coq source tree. Separately, I'm looking at how a Coq platform installation is set up. In part, my goal is to understand the details well enough so that I can add something useful to the documentation (explanation of config behavior/concepts with some best practice suggestions).

[silene]

How do you install it with opam or otherwise?

The list of Opam packages for Coq is available at https://coq.inria.fr/opam/www/

If you filter for fiat, you will notice that the packages are available in the extra-dev suite. This means that you need to do the following before the packages show up in Opam:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

But note that, if the packages are only available in extra-dev, it means that their maintainers consider that they are not fit for users. Presumably, they only exist for the sake of Coq's developers and running the bench.

[jfehrle]

Thanks, that should covered better in the doc. The install for fiat-crypto failed because the jq binary is not installed by Coq platform on Windows (as it is on Linux). And I see conf-jg is not listed in the Coq package index. Is it common for opam package installations to fail? What should the doc tell users to expect?

$ opam install coq-fiat-crypto
The following actions will be performed:
  ∗ install coq-rewriter    dev [required by coq-fiat-crypto]
  ∗ install coq-coqutil     dev [required by coq-fiat-crypto]
  ∗ install conf-jq         1   [required by coq-fiat-crypto]
  ∗ install coq-fiat-crypto dev
===== ∗ 4 =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of conf-jq failed at "dash.exe -ec  jq --version".mcoq-rewriter make]
∗ installed coq-coqutil.dev
∗ installed coq-rewriter.dev

[silene]

And I see conf-jq is not listed in the Coq package index.

This is a standard Opam package, so there is no reason for it to appear in the index of Coq libraries. It appears in the index of Opam packages: https://opam.ocaml.org/packages/conf-jq/

Is it common for opam package installations to fail?

Sure. This is especially true of conf-foo packages, since their purpose is not to install software, but to make sure that some system component is up and running. As the description of conf-jq states, "this package can only install if the jq binary is installed on the system."

[Zimmi48]

Note that there are discussions about including fiat-crypto in the Platform (and therefore in the released opam packages): coq/platform#178