GeoCoq

A formalization of geometry in Coq.

This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.

Details and installation instructions can be found here.

Bug reports are to be submitted here.

It is possible to contact the authors of the GeoCoq library using our mailing list.

GeoCoq is available as releases packages.

Building and installation

• To get the required dependencies, you can use opam.

  • To pin pin the development packages.

    • opam pin -n .

  • GeoCoq relies on other released packages that need to be added.

    • opam repo add coq-released https://coq.inria.fr/opam/released

  • The required dependencies can now be installed:

    • opam install ./coq-geocoq-coinc.opam --deps-only to get the GeoCoq Coinc dependencies;
    • opam install ./coq-geocoq-axioms.opam --deps-only to get the GeoCoq Axioms dependencies;
    • opam install ./coq-geocoq-elements.opam --deps-only to get the GeoCoq Elements dependencies;
    • opam install ./coq-geocoq-main.opam --deps-only to get the GeoCoq Main dependencies;
    • opam install ./coq-geocoq-algebraic.opam --deps-only to get the GeoCoq Algebraic dependencies;
    • opam install ./coq-geocoq.opam --deps-only to get the GeoCoq dependencies.

• The general Makefile is in the top directory.

  • make : compilation of the Coq scripts (after using ./configure.sh).

• Dune can used for compilation.

  • dune build

• You may also rely on dune to install just one part. Run:

  • dune build coq-geocoq-coinc.install to build only the GeoCoq Coinc part (and its dependencies);
  • dune build coq-geocoq-axioms.install to build only the GeoCoq Axioms part (and its dependencies);
  • dune build coq-geocoq-elements.install to build only the GeoCoq Elements part (and its dependencies);
  • dune build coq-geocoq-main.install to build only the GeoCoq Main part (and its dependencies);
  • dune build coq-geocoq-algebraic.install to build only the GeoCoq Algebraic part (and its dependencies);
  • dune build coq-geocoq.install to build only the GeoCoq part (and its dependencies).