Git Product home page Git Product logo

math-comp's Introduction

The Mathematical Components repository

This repository holds the Mathematical Components Library for the Coq system: an extensive body of mathematics formalized in the Coq/SSReflect language.

It also contains the proof of the Odd Order Theorem, that builds on top of the Mathematical Components Library.

Layout and compilation of the library

The library is divided into packages which group together related files. Each package defines a distribution and compilation unit.

Packages can be compiled using the traditional make utility or the more recent OPAM one.

We provide a convenience root Makefile in order to compile all packages at once using make. This is the simplest option.

We also provide opam files to compile each package using OPAM. Note that the OPAM packages for the Mathematical Components library are available in the standard Coq OPAM repositories, under the coq-mathcomp- name space. If you are only interested in installing a Mathematical Components package via OPAM, follow the standard instructions available on the Coq website.

Compilation and installation with make

The instructions assume you are in the mathcomp directory and that you have a supported version of Coq. The list of Coq versions that are known to work can be obtained with:

ls ssreflect/plugin/

Alternatively, if you are familiar with the OPAM slang:

grep depends: ssreflect/opam

If coqc is in your PATH, then you are good to go. Alternatively you can export the COQBIN variable to tell make where the coqc binary is:

export COQBIN=/home/gares/COQ/coq/bin/

To compile the entire library just type make. If you have parallel hardware then make -j 3 is probably a faster option.

The files can be edited using CoqIDE or Proof General, or any other editor that understands the _CoqProject file, with no further configuration from the mathcomp directory.

coqide ssreflect/div.v

Note that you may need to enable _CoqProject processing in your editor (e.g. the default for CoqIDE is to ignore it).

To install the compiled library, just execute make install.

Compilation and installation with OPAM

The instructions assume you are in the mathcomp directory and that you have OPAM installed and configured with the standard Coq repositories.

For each package, pin the opam file:

opam pin -n add ssreflect

This can be achieved in one go as follows:

for P in */opam; do opam pin -n add ${P%%/opam}; done

Then you can use opam install to compile and install any package. For example:

opam install coq.8.5.dev coq-mathcomp-ssreflect

math-comp's People

Watchers

 avatar  avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.