Make Iris and std++ part of the Coq platform

[RalfJung]

I was told opening an issue here is the right way to apply for Coq platform membership, so here we go. :)

I'd like to see Iris and its sole dependency, std++, added to the Coq platform. We (the Iris and std++ teams) promise to do our best to release new compatible versions of our libraries quickly after a Coq release. For Coq 8.12, we actually are faster than Coq itself, having just released Iris 3.3 and std++ 1.4 which are already compatible with the upcoming Coq 8.12 (tested against the current 8.12 git branch).

I am not sure if we need to demonstrate "sufficient public interest" or so, but if we do, I hope https://iris-project.org/ is convincing enough that Iris indeed is already seeing numerous interesting applications.

[RalfJung]

@MSoegtropIMC any news for Iris and std++ to become part of the platform?

[MSoegtropIMC]

I first want to get the beta1 with the set included in the 8.12 Windows installer out before I add additional things.

My current working point is merging all my local opam patches required to make the beta1 work upstream. After that I will look into new packages. I need to limit the number of open threads I have.

[RalfJung]

Any news on this? 8.12 is out for quite a while and 8.13 is getting closer. :)

Half a year ago we were told to report an issue here to start the process of including Iris in the coq-platform, but so far not much has happened.

[MSoegtropIMC]

Well getting the first version of platform ready was a bit more work than expected. Especially the various Linux distros are a nightmare where things fail arbitrarily. But this is mostly fixed now. I hope to make good progress with the packages from now on. It should be ready in time for 8.13.

[Zimmi48]

The Windows installer for the 8.13 release is now based on the platform (see https://github.com/coq/coq/releases/tag/V8.13%2Bbeta1) but AFAIU it is still with the initial set of packages (coming from the previous installer) so it doesn't yet include Iris...

[MSoegtropIMC]

Yes. I am a bit unsure about priorities:

• Add additional packages
• Create platform based Mac installer
• Do final release tests for 8.12.1.0
• Test Coq on macOS BigSur
  Essentially right now I am doing all of this in parallel

[Zimmi48]

Create platform based Mac installer

This is the big next step IMHO, from the Coq development team point of view. In particular:

• we are currently relying on fragile infrastructure for generating the macOS package as many bad events happening just before a release have shown;
• we currently have a process to sign packages, but not for notarization (see coq/coq#12760);
• we currently have a signing certificate but no clear process for renewing it (it was bought when the Coq Consortium was part of the Inria Foundation). Contrary to the Windows installer for which there is a person in charge of signing at Inria, there is no equivalent process for macOS (AFAIK).

We hope that you being at Apple can help us make progress on these issues...

(But better to take this discussion somewhere else if it should continue, because that's not the topic of this issue.)

[MSoegtropIMC]

(But better to take this discussion somewhere else if it should continue, because that's not the topic of this issue.)

Well half - it is part of the priority discussion. But I guess a decent Mac OS installer is a bit more work - for this reason it would make sense to now spend some time on the additional packages. My plan is to release Coq platform 8.12.1.0 with the packages as is and do an 8.12.1.1 release with extended package set soon after. I am currently testing (especially on MacOS BigSur). I think about doing some Mac homebrew tests before the release.

[Zimmi48]

Sounds good to me. Note that there are talks of an 8.12.2 release (see coq/coq#13599). We will discuss this topic in the Coq Call today.

[RalfJung]

FWIW, we have released a version of Iris that is compatible with Coq 8.13, so we're ready to become part of the corresponding platform. :D

[MSoegtropIMC]

I added Iris and std++ to an updated pick for 8.13 in Coq Platform 2021.09 in PR #143.

I added both to the "full" level (not the larger and less strict "extended") level.

I plan to add it to 8.14 as well, but I would need a tag compatible with 8.14+rc1 preferably within 4..6 weeks.

[MSoegtropIMC]

P.S.: as test files for the Coq Platform "smoke test kit" I randomly selected these files:

TEST_FILES[coq-iris]='tests/heapprop.v'
TEST_FILES[coq-stdpp]='tests/sets.v'

Please feel free to suggest other files. The smoke test kit is mostly there to test if a package has been properly installed and is basically working. Several files per package are possible, but the total run time should be no more then a few seconds (<10). It helps maintenance, if the file doesn't change in each version ;-)

[RalfJung]

Thanks a lot! Our git master branch is compatible with Coq 8.14, but we would usually do our release closer to or even just after the Coq release. Would that work or do you require an earlier release?

It helps maintenance, if the file doesn't change in each version ;-)

I assume you mean the filename -- it is okay if the contents change?
Another good test file for Iris would be tests/one_shot.v.

[MSoegtropIMC]

I am currently working on an updated and extended package pick for Coq 8.13. For 8.14 it would be perfect to have a tag 2 weeks after Coq 8.14.0 release. The 8.13 pick will be released fairly soon, though. Coq Platform now support several different "versions", that is several Coq versions and also sometimes for one Coq version several package picks.

I assume you mean the filename

yes, I mean file name and path - the contents can of course change. I will add the file you suggested.

[MSoegtropIMC]

@RalfJung : I have a rather weird CI error: A coq file fails to compile on Windows:

https://github.com/coq/platform/pull/143/checks?check_run_id=3704943519#step:5:1718

Are you aware of this or do you have an idea what the root cause might be?

[RalfJung]

That looks like a line ending issue to me, which leads to a non-empty diff.
For people getting the source via git, our .gitattributes takes care of this... but opam uses a tarball. Do you have any idea how to best handle line ending conversion there? The files in the tarball use Unix line endings but it seems on Windows coq outputs Windows line endings and then diff complains about that.

[RalfJung]

Ah, looks like we should use diff --strip-trailing-cr. https://gitlab.mpi-sws.org/iris/stdpp/-/commit/e5b77dc5003acff061d187c868cdde45d64e7d52 should fix the issue on git master, but I am not sure what the best way is to get std++ 1.5.0 fixed (and Iris has the exact same problem).

[MSoegtropIMC]

I tend to use tr to remove the carriage returns, but the diff option you found is a very nice solution!

For such small changes, I think it is OK the include a patch in the opam file - I can do this.

[MSoegtropIMC]

@RalfJung : including your change as an opam level patch works fine. I guess there are no objections against pushing this to the main opam repo (I could keep it in the Coq Platform local patch repo also) ? According to the opam rules one wouldn't have to change the version number, since it changes nothing on systems on which it did work before and fixes issues on systems where the install aborted before.

iris installs fine without changes after the fix to stdpp.

[RalfJung]

I have no objections to pushing this patch to the Coq opam repository.

iris installs fine without changes after the fix to stdpp.

That is strange, it uses the exact same kind of test suite.

[MSoegtropIMC]

That is strange, it uses the exact same kind of test suite.

Usually opam does not run the test suite, though.

It is possible that stdpp runs a small piece of this during the normal build. Actually with stdpp the failure is very early, within a few seconds - the build takes quite a bit longer It is quite possible that we need the same patch for iris in case opam is instructed to run the tests.

[RalfJung]

Usually opam does not run the test suite, though.

We run it as a regular part of make.

But I realized the reason: the Iris repository actually contains multiple opam packages, so it has a somewhat different setup to build and install just the part for one package. The test suite does not belong to any of the packages, so it is not run on opam.

This is a reorganization that we did since I originally created this issue. It means that the coq-iris-heap-lang package is now separate -- would it be possible to include that in the Platform as well? It is released together with coq-iris, but not all Iris users want or need HeapLang so we split it into a separate package.

[MSoegtropIMC]

Sure, assuming coq-iris-heap-lang doesn't result in hard to solve CI issues, I will add it.

[MSoegtropIMC]

@RalfJung : can you please suggest a "smoke test kit" example file for coq-iris-heap-lang?

[MSoegtropIMC]

(and one for coq-iris, I am currently using tests/heapprop.vwhich might be for coq-iris-heap-lang)

[MSoegtropIMC]

I included coq-iris-heap-lang with PR (#144).

So the only thing missing is a clarification on the smoke test files.

[RalfJung]

tests/one_shot.v actually requires HeapLang already. (In contrast, tests/heapprop .v does not... yeah the names are a bit confusing.)

[MSoegtropIMC]

Hmm, for that I get:

File "./one_shot.v", line 4, characters 50-55:
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix iris.deprecated.program_logic.

[RalfJung]

Ah right... maybe better to use tests/heap_lang.v then, sorry for this.

[MSoegtropIMC]

Thanks, this works! It is all set then and I will close this issue.