Skip to content

Latest commit

 

History

History
117 lines (114 loc) · 9.28 KB

TODO.md

File metadata and controls

117 lines (114 loc) · 9.28 KB

  • OPAM

    • figure out why installation of opam install coq-corn.8.6.dev and opam install coq-corn.dev currently never terminate.

  • intuitionistic-nuprl is also being maintained elsewhere. We should check it out; compare to our version and decide whether it make sense for us to maintain our version (separately).

  • add the proof of Puiseaux theorem

  • intuitionistic-nuprl

    • needs a proper Makefile and Make

  • Clarify the purpose of coq-contribs.

    • It should be clear that if something is being actively worked on, it is not something anybody would want to include into coq-contribs.
      • Coq-contribs are diverse developments which are interesting but, sadly, no longer maintained by their original authors.
      • Coq-contribs is a place to preserve them to keep track of interesting things that were done in the past.
    • They also have less poetic purpose --- we can use them for testing/benchmarking current commits. E.g. today I see that commit e9c57a3 changed the behavior of coq_makefile in such a way that several coq-contribs no longer compile. Very possibly non-coq-contribs will not compile also and we see that something is not right.

  • Fix intuitionistic-nuprl on trunk.

  • Add the following new coq-contribs:

    • mmultisets (currently, it depends on something which was not yet ed and so the version we have is not compilable)
      • it depends on MMaps which was not yet released (Pierre Letouzey (?) might know something more about it)
    • mirror-core
    • HoTT

  • Go through existing coq-contribs:

    • identify those ones which have no licence
    • ask the author(s) whether this intentional or perhaps just an omission

  • There is an overlap between "description" and "opam" files. Can't we somehow refactor this information?

  • Remove the branch = ... lines from .gitmodules

  • The information in the description files should be properly structured and we should be able to mechanically "validate" it.

  • Go over categories declared by individual coq-contribs. Refactor and document them.

  • Go over tags declared by individual coq-contribs. Refactor and document them.

  • Go over licences declared by individual coq-contribs. Refactor licence names and provide links to the corresponding texts.

  • Convert .svnignore to .gitignore.

  • Add missing .gitignore files.

  • high-school-geometry:

  • add lemma-overloading among the tracked coq-contribs. Problems:

    • it depends on math-comp
    • the master branch of lemma-overloading does not compile with Coq trunk.

  • merge this pull-request to opam-coq-archive

  • web pages related to coq-contribs need to be updated (?), merged (?), migrated (?)

  • Increase the consistency of names:

    • *-theory
      • graph-theory
      • set-theory
      • group-theory
      • ... ?
    • *-geometry
      • constructive-geometry
      • euclidean-geometry
      • high-school-geometry
      • projective-geometry
      • ruler-compass-geometry
      • tarski-geometry
      • ... ?
    • *-arithmetic
      • e.g. we might want to rename presburger to presburger-arithmetic
    • *-theorem
      • ... ?

  • refactor coq-contribs

  • figure out why -j32 does not work with ergo

  • For each coq-contrib check if there exists an upstream version.

  • we should write a "lint" script that will probably check the expected properties of coq-contribs as we have informally defined them here

  • Go over all OPAM packages. Those that are marked "proprietary" should not be released before we settle the licence issues.

  • Individual coq-contribs should have a nice, browsable and cross-referenced source-code presentation.

  • Convert Make files into _CoqProject files (proof-general and coqide both take it into consideration)

  • Change the names of repositories (and OPAM packages) that they correspond to directory name under which they are installed in the user-contribs directory.

  • All coq-contribs should have a README.md file.

  • Check why we currently see warning: option -slash has no effect and is deprecated

  • Check all warnings that are currently generated when compiling coq-contribs

    • Convert all warnings to errors.

  • Why we have sum-of-two-square? Why not sum-of-two-squares?

  • Jenkins

    • record in some useful way information about build-times of individual coq-contribs (and the Coq itself) on individual branches (v8.5, v8.6, ..., trunk) as Coq evolves

    • our Jenkins job that test installability of OPAM packages should not stop at the first failure but instead they should continue and test the rest of the packages.

    • our Jenkins jobs should also test uninstallability of individual packages (we do not do this because there is some strange bug in OPAM which makes it behave in a wrong way with --root parameter in case we are uninstalling a package)

    • at the moment, URLs of the results of jobs have little clues about:

      • who started the job
      • which Coq branch was used It would make sense to include this kind of information into the job's name.

    • figure out how could we allow anyone to run Jenkins job without security risks

    • more descriptive names for the jobs we run should be generated at run-time (instead of numbers).

    • We already symbolically track dependencies of individual coq-contribs. We might reuse that information and instead of hardcoding the "dependencies" of individual coq-contribs in the following Jenkins jobs:

      we might as well generate those jobs with from those dependencies.

    • Once we fix this, we will want to remove the corresponding workaround from the /home/jenkins/bin/opam-install-package file on pyrolyse node. Now, we use -j1 instead of -j32 for certain packages:

      • legacy-ring
      • legacy-field
      • string

      for which -j32 would cause a spurious compilation error (due to the bug).

  • Figure out what can we do with lemma-overloading. It now depends on math-comp which is not part of coq-contribs.

  • describe all the steps that need to be performed when we add a new coq-contrib

    • concerning the git repository
    • concerning our jobs on Jenkins

  • describe all the steps that need to be performed when a new Coq branch is created (e.g. v8.7)

  • describe all the steps that need to be performed when a new version of Coq is released

  • rename OPAM package coq-coq-in-coq to coq-in-coq

  • figure out why make uninstall command in individual coq-contribs does not work.

  • check what do we say in README files (whether all the things we say are still valid; whether the provided information is complete)

  • consider, whether we still need the description files; did not the opam files serve the same purpose?

  • explain how coq-contribs can be installed via OPAM.

    • would a sentence like the one we added here suffice?
    • add a link to those instructions to README.md files that belong to individual coq-contribs.

  • figure out the most convenient way to launch coq-contrib job on Jenkins for a given (Coq) pull-request

  • figure out the most convenient way to lauch coq-contrib job on Jenkins for a given (coq-contrib) pull-request

  • what do we want to do with the old git repositories? Does it makes sense to keep them? Now they are behind their github counterparts. Do we want to turn them into mirrors?

  • when people try to Google out coq-contribs, they find this. We may want to put there redirection to some more proper location.

  • go through OPAM packages that correspond to individual coq-contribs (for individual Coq version) and run opam lint with them. Fix all warnings and errors.