search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
187 stars 48 forks source link

Coq platform for research artifact evaluation #2

Open palmskog opened 4 years ago

palmskog commented 4 years ago

The research communities around programming languages, formal methods, and software engineering are continually expanding and improving artifact evaluation for their premier conferences. Some examples:

The Coq platform is a natural focal point for research artifacts based on Coq and OCaml. Researchers can potentially target a Coq platform version for their submitted artifact, and this platform version is then used by the committee during artifact evaluation, which minimizes packaging and distribution effort for both parties, and ensures reproducibility. The Coq platform can also provide a format for packaging the artifacts for long-time archiving.

However, Coq platform maintainers will likely have to coordinate with artifact evaluation committee chairs so that the Coq platform is permitted as part of mandated evaluation environments. For example, a virtual machine may be mandated which does not directly support the Coq platform without significant work by the submitting researchers.

Since the POPL AE traditionally has many Coq artifacts, e.g., around 10 out of 40 artifacts submitted during 2019, coordinating with the chairs of that committee is a natural first step.

spitters commented 4 years ago

As do CPP and ITP of course.

palmskog commented 4 years ago

To my knowledge, neither CPP nor ITP have a dedicated artifact evaluation committee, and doesn't currently provide any guidelines that restrict how artifacts are submitted or handled by any committees. This is why I believe we would have much better success in getting Coq platform adoption to the POPL artifact evaluation.

tchajed commented 4 years ago

This would be great; just to add more data, in POPL 2020, 17 out of the 40 artifacts used Coq.

MSoegtropIMC commented 2 years ago

@palmskog : I am not sure what to do about this. Would you consider this solved by the recent paper by you, @gares and @Zimmi48 ?

palmskog commented 2 years ago

@MSoegtropIMC our paper is only one piece of the puzzle in convincing venues such as TACAS, CPP, etc., to recommend submissions to use the Platform whenever they have a Coq artifact. I expect that the academic side of the Platform team will have to "evangelize" using the Platform for several years more. Hence, I think we should keep this issue open to track progress.

MSoegtropIMC commented 2 years ago

OK, I created a milestone "Longterm"

palmskog commented 1 year ago

For the record, I counted 9 out of 25 accepted CPP 2023 papers using Coq: https://popl23.sigplan.org/home/CPP-2023#event-overview

MSoegtropIMC commented 1 year ago

Do you also have statistics for the other proof systems?

palmskog commented 1 year ago

In CPP 2023, there were:

palmskog commented 9 months ago

In CPP 2024, there are:

spitters commented 9 months ago

We're certainly working on getting our work on the Last Yard paper in CI: https://eprint.iacr.org/2023/185 We'd like to upgrade it to MC 2.0 and would like to get better CI for jasmin (I forgot what precisely).

spitters commented 9 months ago

Have you contacted any of the authors of the accepted papers? https://popl24.sigplan.org/home/CPP-2024#event-overview

palmskog commented 9 months ago

@spitters I don't really have cycles for that kind of outreach. My somewhat modest goal would be that CPP Coq artifacts are archived on a service like Zenodo along with instructions on how to reproduce them using a specific release/pick of the Coq Platform. If artifacts are made reusable and developed further with CI best practices, this is nice, but the baseline should be easy reproducibility.

snyke7 commented 9 months ago

I am in the process of packaging an artifact for CPP 2024 and saw this thread on the Coq zulip. In my case, the artifact depends on a library that is not part of the Coq Platform (coq-library-undecidability). I would usually package artifacts with a custom script and explicitly listed opam dependencies, packaged both as a source folder and as a virtual machine.

How should I go about in making my artifact reproducable with a specific release/pick of the Coq/Platform, when my artifact depends on a non-platform library?

I tried to make install the library I need, but that does not work since the snap is read-only. I suppose I could make a customized package pick but that sounds like more (compilation) work than what I did before. I could also make _CoqProject point to a local clone of the library.. but I don't think that is ideal either.

palmskog commented 9 months ago

@snyke7 we don't have a ready-made solution for this scenario, you have several options:

MSoegtropIMC commented 9 months ago

@snyke7 : The advantage of a customised package pick is that it is a one file references of what you need. I would also remove everything yo don't need from the pick, so that building is fast.

I would not use snaps or the like - many people have difficulties using snaps. The script takes a while to run, but it is a very reliable and multi platform way to distribute a Coq environment.

So you should distribute a tailored pick file + Coq Platform release version number (to specify the script and opam patch base).

Custom installers are more intended for large audience lectures and IMHO not the right tool for research artifact reproduction.

You can btw. also simply distribute an opam file of your project stating the proper dependencies. People having opam ready can use this, and for people without opam, the scripts are the most flexible and reliable method, even though it takes a while.

snyke7 commented 9 months ago

Thanks for your replies! I am not sure how people are using the Coq Platform if not through the snap, do they have a local clone of the Coq Platform repository?
Anyway, my approach for a relatively self-contained artifact will now be to:

  1. Include the latest release of the Coq Platform repository
  2. Create a custom pick file, with just the packages I need
  3. Include an opam file for non-platform users

It would be ideal for future artifact packagers if 2 could be derived from 3 or vice-versa.

MSoegtropIMC commented 9 months ago

I am not sure how people are using the Coq Platform if not through the snap

Expert users - and people looking at research artefacts belong here - should use the scripts (or opam) because the scripts give more flexibilty. The binary deliveres, including snap, are mostly intended for lectures.

I don't think you need to include the Coq Platform release verbatim - a reference to the tar ball should do.

Converting pick files to/from opam is not entirely trivial, because they contain different meta information, but it might be possible to create a pick file from an opam package with minimal user interaction. The reverse is likely not feasible.

MSoegtropIMC commented 2 months ago

I would say this is solved by the publication of https://arxiv.org/abs/2203.09835, so I am closing this.

palmskog commented 2 months ago

@MSoegtropIMC I personally don't think this is a solved issue, since we haven't been able to convince conferences/journals to at least recommend (much less require) supporting the Platform for Coq papers/artifacts.

MSoegtropIMC commented 2 months ago

@palmskog : please feel free to reopen. It is just so that I am not that close to research so I don't really know what to do about this. I am also not sure if this is the right place to discuss such things. I guess a discussion on Zulip would have more impact - very few people are reading this here.

palmskog commented 2 months ago

I agree we can discuss research-related issues on Zulip, but I think it's very convenient to have this issue for tracking progress. Certain conferences may have specific requirements before they recommend the Platform.