Stepping through HoTT files in a IDE with an opam installed HoTT (regression)

[MSoegtropIMC]

For beginners it is helpful if they can step through files from HoTT in an IDE with an opam installed HoTT.

This generally requires that the requires commands name the library, say via "From HoTT Require".

Up to the 8.19 version this was the case, but in 8.20 a HoTT prefix has been removed - at least from the one file I use as "smoke test" file in Coq platform, which is theories/Analysis/Locator.v. I now have to patch the require statements with awk, so that the file can be compiled outside of HoTT. This is OK, but as I said the main issue are beginners trying to understand HoTT by stepping through files with an opam installed HoTT.

[Alizter]

When using the HoTT library outside of this project, it is recommended to require things by doing From HoTT Require .... For files inside the project, this is not necessary since we use a _CoqProject file (that is autogenerated) with the correct -R flags. This is documented in README.md, STYLE.md and INSTALL.md.

My suggestion to you for the smoke-test going forward would be to write a test file with the following contents:

From HoTT Require Import HoTT.

This will be a good smoke-test on your end that everything is working correctly. HoTT.v is an indexing file that imports most of the HoTT library, and the name will not change any time soon.

Regarding using From HoTT everywhere, I do sympathise with your point about beginners coming from the Coq Platform trying to step through those files, but I don't think this problem pertains only to us. Coq doesn't require a From prefix for Requires nor is there a mechanism to enforce it.

Doing a big change requiring From everywhere in the library will be very annoying on our end with no big benefit in the long run. It will be difficult to always enforce and will cause on-going developments and PRs to have trivial conflicts.

There is another problem which is -indices-matter and -noinit are not correctly passed to an IDE, so some files will not even work even if we had From HoTT.

[MSoegtropIMC]

There are of course other solutions, but I don't think a generated _CoqProject file will do.

The use case is this:

• User installs HoTT via opam (e.g. via Coq Platform)
• User git clones the HoTT repo
• User does not want to build HoTT (which might be tricky) but step through a HoTT file from the repo using the installed HoTT files

This use case does work with quite a few repos - and it did also work with the previous version of HoTT - at least for some files.

The issue with a _CoqProject file is that it usually points -R to the local folder, not to the opam HoTT. Another issue with _CoqProject files is that there is no way to write a static _CoqProject file which points to a package in the default Coq user-contrib folder.

I find the few letter "From HoTT" before each Require not that bad, and you can setup in the project what this means.

[jdchristensen]

Is there a standard for how to handle this across the Coq community? If the consensus is to put "From LibraryName" before every Import, then I don't mind if we do that here.

However, I don't find the suggested use case very compelling. Stepping through files from the git version of Coq-HoTT using an opam installed version is not supported and is likely to frequently break as various core definitions often change. Moreover, building the library should be very easy, by typing "make" or "dune build", and it's also fast. So, before changing this, I'm wondering if you have any other use cases?

I'll also mention that you can "step through" the proofs by going to the html view of the library produced by alectryon. For casual viewers, that should work, without needing to compile and without issues of version mismatch.

[MSoegtropIMC]

Usually people download a tagged tar ball from git matching the version they have when they just want to look at the sources.

Believe me, there are skilled mathematicians which do find it difficult to compile software. Even if it might just work in a specific situation, there are many situations where it doesn't (e.g. on Windows). As long year maintainer of Coq Platform I had my share of wrestling with "easy to build" packages, and I would call myself an expert in this. Even if things are better for HoTT, many people are just "burned" and first try other ways.

In the HTML view you cannot run querries like Search. I do this frequently.

Is there a consensus? From the 68 packages in the Coq Platform smoke test kit 14 need a patch of the require command. So not everybody does this, but the majority.

[SkySkimmer]

I think we do consider using -R for the current package idiomatic.
If we want installed sources to be IDE compatible we should do it in Coq (ie rocq-prover/rocq#15924) not by messing with random packages.

[MSoegtropIMC]

But to be sure there is no requirement from my side. I just try to give you a hint from my experience as Coq Platform maintainer how you can lower the contact burden for potential users of HoTT. As I said, not everybody who might have bright ideas about homotopy is a skilled software package wrangler.

[MSoegtropIMC]

@SkySkimmer : currently the issue is that there is no way to give a -R option in a static file in a system independent way. I suggested having a -V option which is like -R but goes relative to the coq library path. Together with a _CoqProject file checked into git, this would also work.

But I fully agree that an improvement in Coq to support this use case would be very helpful.

Also note that I reported this because in previous versions of HoTT this did work - it is new that it doesn't.