Karl Palmskog
Karl Palmskog
There have now been several packages in `released` whose archives (tarballs) have become inaccessible either permanently or temporarily (coqhammer-1.0.3 is the [latest example](https://github.com/lukaszcz/coqhammer/issues/58)). One way to deal with this problem...
We [currently](https://coq.inria.fr/opam-packaging.html) use only the following criteria for inclusion of a package in the `released` OPAM repo/index (and some are not always fully enforced): - Includes a Changelog that lists...
It looks like the package `coq-mathcomp-finmap` introduced the following dependency for version 1.2.0: ``` "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1.0~") } ``` However, as far as I can see,...
The OCaml OPAM archive tracks the number of installs for each package (version) and displays this information under the header "Statistics", for example for [Coq 8.10.2](https://opam.ocaml.org/packages/coq/coq.8.10.2/). To measure popularity of...
Since MD5 is known to not be collision resistant, and has been [described](https://www.kb.cert.org/vuls/id/836068/) as "cryptographically broken and unsuitable for further use", I think it's time we actively phase out MD5...
The names of licenses in packages appears to currently be subject to informal conventions (albeit quite uniform such conventions). For example, grepping in `released` repo recently revealed: - 277 `opam`...
This is to document and clarify the use and non-use of `~` and other delimiters in OPAM package versions. As originally defined Debian, the use of `~` in version names...
Using the regular coq_makefile for coq-dpdgraph is a lot of work for an essentially deprecated approach to building Coq plugins. Here is a quick port to Dune instead. The plugin...
After #54 is merged, we need to consolidate some material and possibly reorganize it a bit. I open this issue as a memento. So far, we have at least the...
#### Description of the problem The following self-contained code using Equations yields either an incomprehensible error (`Variable k should be bound to a tactic.`) or a plain anomaly (`Anomaly "Uncaught...