coq-community / stalmarck Goto Github PK

Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

License: GNU Lesser General Public License v2.1

Coq 97.70% Makefile 0.06% OCaml 2.25%

coq-extraction coq-plugin coq docker-coq-action nix-action coq-ci tautology-checking tautology

stalmarck's Issues

Patent warning appears to be obsolete

The README contains a warning about the patented status of the algorithm. As far as I can see, the patents have all now expired.

Specifically, the patents are: Swedish Patent No. 467,076 (approved 1992); U.S. Patent No. 5,276,897 (approved 1994); European Patent No. 403,454 (approved 1995).

stalmark (master) is not compatible with any released version of Coq!

It has been adapted to EConstr, but the porting to 8.7 was not completed.

Extracted code is checked into version control

The staltac tactic is produced from code in version control that was previously extracted, then manually copied into an OCaml file, and mixed with imperative code. The proper way to do this is to have a project build extract the relevant code every time, and link it with the imperative code to produce the tactic.

Recommend Projects