Repository structure

[yforster]

After discussion with Andrej, here's a proposal how to structure the repository in the future in order to be most easily to maintain. Please add your thoughts from a user perspective (@DmxLarchey, @dominik-kirst, @fakusb).

---

Change 1: There will only be one branch. A configure.sh script can be used to locally set up the repository for either a minimal use (no opam, no external libraries) or a full use. This is done by shipping a _CoqProject.minimal file and a _CoqProject.full file. In the minimal case, the first file is used, in the full case, both files are appended by the configure script.

Change 2: We move to a "one directory per problem class" structure. I.e. the structure will look as follows:

• Directory PCP
  • File PCP.v containing the definition of PCP, File PCP_undec.vcontaining a statement PCP_undec : Halt <= PCP.
  • File BPCP.v containing the definition of BPCP, File BPCP_undec.vcontaining a statement BPCP_undec : Halt <= BPCP.
  • more files for problems similar to PCP
  • auxiliary files, possibly in subdirectories

The current Problems directory goes away, so does the Reductions directory. The Shared directory stays as is.

Using this setup, it should be relatively easy to write Makefile targets such that one can do make PCP and only get the PCP directory (and all recursive dependencies) compiled, reducing compile time for users that only want to use part of the library.

---

This way, if a user wants to import a problem, they have to do Require Import ProblemClass.Problem, e.g. PCP.MPCP or Rewriting.SR. If they want to import the full reduction to this problem, it's Require Import ProblemClass.Problem_undec.

[DmxLarchey]

In complement, I have been thinking about the proposal of a Wiki by Andrej which is a good idea. However, it seems we are facing the usual issue when describing a graph: do we do it by the edges or by the vertices. Right now, it is by the vertices but I suggest that we move to both. What I mean is that ideally, we would have a real graph with hyperlinks:

• when you click on an edge, a page is generated which contains the description of the source and destination problems for this edge together with information about this reduction.
• when you click on a vertex, a page is generated containing a description of the problem and a list of adjacent edges with corresponding links.

I am not sure how to implement such a interface. Could we put in place a database? What do you think ?

[fakusb]

Concerning the code organisation: In my opinion, the main goal of such a refactoring is to increase reusability of parts. So collecting all problems, definitions etc. related to PCP in the "PCP" folder seams very reasonable. But where to put reductions between two problems, for example 'DIO_SINGLE_SAT ⪯ MUREC_HALTING'?

Except that, I agree with Yannicks proposed changes.

[yforster]

Regarding Change 1: MetaCoq is now following Coq master, which means that we can release an opam package immediately for every new Coq version. I have ported the library to Coq 8.10 (on branch coq-8.10) and to 8.11 (on branch coq-8.11), without major hurdles, and I think it would be great if we could try to have the library working for every new Coq version as well.

All dependency management is done via opam and there is no external directory anymore and no submodules. For now some opam packages are in an opam repository maintained by us for quicker testing, but we can move them to the official repository once we've merged all of the PRs that are open.

I thus propose the following new structure of branches:

• the current master becomes coq-8.9, but does not receive new updates. We do not care about Coq 8.8 anymore.
• the current coq-8.10 branch stays and maybe gets some cleaning updates, but at a point in the near future it also stops receiving update
• the coq-8.11 branch becomes our main branch for new updates (and is the branch people see when they click on the github repo or clone it)
• the noopam branch stays alive. It tries to be as compatible with as many Coq versions as possible (but definitely the most recent one) and has no external dependencies

I'm aware this is yet again another change of the branch structure, but my hope is that this makes it easiest to update the library to new Coq versions in the future.

@DmxLarchey @mrhaandi What do you think?

[yforster]

Regarding Change 2, Andrej started working on bringing some of the most important problems into this shape, which I think is great.

I am not sure how to implement such a interface. Could we put in place a database? What do you think ?

I am not sure either. For the short term the most reasonable goal is to have a wiki describing both edges and vertices. If we can get something graphical allowing the user to click and then end up on the right page of the wiki that would be great, but a wiki would already be a first step. (I'm aware that for many problems I myself should start writing wiki pages, it's on my TODO list for a long time already but didn't move much since then)

I found that discussing issues like this sometimes is quicker in a Skype/Zoom meeting, which I've been using a lot with Andrej and Fabian to get the porting done. Maybe it makes sense to schedule a Zoom undecidability library meeting, just to sync and discuss what's up next? Even if it's just 15 minutes, it might be more efficient than GitHub issues

[mrhaandi]

@DmxLarchey @mrhaandi What do you think?
I fully support this.

[DmxLarchey]

Maybe it makes sense to schedule a Zoom undecidability library meeting

Yep and maybe you could add Dominik as well ?

[mrhaandi]

After a cleanup of SemiUnification according to design guidelines discussed with Yannick, I have summarized the main principles in the Wiki:
https://github.com/uds-psl/coq-library-undecidability/wiki/Structure-Guidelines
Feel free to discuss and extend. Those could be useful for external contributors, but also to keep track ourselves.

[yforster]

These are the directories which do not follow the structure guidelines at the moment:

• MuRec
• TRAKHTENBROT
• HOU

That's not so bad! :) I don't think we have to fix this for the 1.0.0 release, but it's good to keep track.