math-comp / real-closed

Theorems for Real Closed Fields
13 stars 11 forks source link
coq mathcomp real-closed-fields ssreflect

Real closed fields

Docker CI

This library contains definitions and theorems about real closed fields, with a construction of the real closure and the algebraic closure (including a proof of the fundamental theorem of algebra). It also contains a proof of decidability of the first order theory of real closed field, through quantifier elimination.

Meta

Building and installation instructions

The easiest way to install the latest released version of Real closed fields is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-real-closed

To instead build and install manually, do:

git clone https://github.com/math-comp/real-closed.git
cd real-closed
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

The repository contains

Except for the end-results listed above, one should not rely on anything.

The formalization is based on the Mathematical Components library for the Coq proof assistant.

Development instructions

With nix.

  1. Install nix:

    • To install it on a single-user unix system where you have admin rights, just type:

    sh <(curl https://nixos.org/nix/install)

    You should run this under your usual user account, not as root. The script will invoke sudo as needed.

    For other configurations (in particular if multiple users share the machine) or for nix uninstallation, go to the appropriate section of the nix manual.

    • You need to log out of your desktop session and log in again before you proceed to step 2.

    • Step 1. only need to be done once on a same machine.

  2. Open a new terminal. Navigate to the root of the Abel repository. Then type:

    nix-shell

    • This will download and build the required packages, wait until you get a shell.
    • You need to type this command every time you open a new terminal.
    • You can call nixEnv after you start the nix shell to see your work environemnet (or call nix-shell with option --arg print-env true).
  3. You are now in the correct work environment. You can do

    make

    and do whatever you are accustomed to do with Coq.

  4. In particular, you can edit files using emacs or coqide.

    • If you were already using emacs with proof general, make sure you empty your coq-prog-name variables and any other proof general options that used to be tied to a previous local installation of Coq.
    • If you do not have emacs installed, but want to use it, you can go back to step 2. and call nix-shell with the following option

      nix-shell --arg withEmacs true

      in order to get a temporary installation of emacs and proof-general. Make sure you add (require 'proof-site) to your $HOME/.emacs.