diff options
| -rw-r--r-- | AUTHORS (renamed from etc/AUTHORS) | 0 | ||||
| -rw-r--r-- | CeCILL-B (renamed from etc/CeCILL-B) | 0 | ||||
| -rw-r--r-- | ChangeLog (renamed from etc/ChangeLog) | 0 | ||||
| -rw-r--r-- | etc/INSTALL.md | 78 | ||||
| -rw-r--r-- | etc/Makefile | 6 | ||||
| -rw-r--r-- | etc/README | 40 |
6 files changed, 0 insertions, 124 deletions
diff --git a/etc/ChangeLog b/ChangeLog index 12d6ef4..12d6ef4 100644 --- a/etc/ChangeLog +++ b/ChangeLog diff --git a/etc/INSTALL.md b/etc/INSTALL.md deleted file mode 100644 index 4bc3a95..0000000 --- a/etc/INSTALL.md +++ /dev/null @@ -1,78 +0,0 @@ -# INSTALLATION PROCEDURE - -Users familiar with OPAM can use such tool to install Coq and the Mathematical Components library with commands like - - opam repo add coq-released http://coq.inria.fr/opam/released - opam install coq-mathcomp-fingroup - -This document is for users that installed Coq in another way, for example -compiling it from sources. - -## REQUIREMENTS - -Coq version 8.5 to 8.7.0 - -## BUILDING - -The Mathematical Components library is divided into various installation -units. On can install the entire library (compilation time is around 35 minutes) or only some of its units. - -In both cases, if Coq is not installed such that its binaries like `coqc` -and `coq_makefile` are in the PATH, then the COQBIN environment variable -must be set to point to the directory containing such binaries. -For example: - - export COQBIN=/home/user/coq/bin/ - -Now, to install the entire library, including the SSReflect proof language: - - cd mathcomp-1.6/mathcomp - make -j2 && make install - -If one wants to only install a few modules he should instead run make -inside the modules he wants to install *in the following order*: - - 1. ssreflect - 2. fingroup - 3. algebra - 4. solvable - 5. field - 6. character - -This means that one cannot install, say, algebra without having already -installed fingroup. An example: - - cd mathcomp-1.6/mathcomp - cd ssreflect && make -j2 && make install - cd ../fingroup && make -j2 && make install - -## CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE - -The `mathcomp/ssreflect/` directory comes with a small configuration file -`pg-ssr.el` to extend ProofGeneral (PG), a generic interface for -proof assistants based on the customizable text editor Emacs, to the -syntax of ssreflect. - -The >= 3.7 versions of ProofGeneral support this extension. - -- Following the installation instructions, unpack the sources of PG in -a directory, for instance <my-pgssr-location>/ProofGeneral-3.7, and add -the following line to your .emacs file. -Under Unix/MacOS: - - (load-file - "<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" ) - (load-file "<my-pgssr-location>/pg-ssr.el") - -Under Windows+Cygwin: - - (load-file - "C:\\<my-pg-location>\\ProofGeneral-3.7\\generic\\proof-site.el") - (load-file "<my-pgssr-location>\\pg-ssr.el") - -Where <my-pg-location> is the location of your own ProofGeneral -directory, and where <my-pgssr-location> is the location of your pg-ssr.el -file. - -Coq sources have a .v extension. Opening any .v file should -automatically launch ProofGeneral. diff --git a/etc/Makefile b/etc/Makefile deleted file mode 100644 index 5515da0..0000000 --- a/etc/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -VERSION=$(shell git symbolic-ref --short HEAD | cut -d / -f 2) - -dist: - cd ..; git archive --format tar --prefix mathcomp-$(VERSION)/\ - -o mathcomp-$(VERSION).tar HEAD - cd ..; gzip -f -9 mathcomp-$(VERSION).tar diff --git a/etc/README b/etc/README deleted file mode 100644 index 4d33be7..0000000 --- a/etc/README +++ /dev/null @@ -1,40 +0,0 @@ - THE MATHEMATICAL COMPONENTS LIBRARY - ------------------------------------------ - - -DOCUMENTATION -============= - - The documentation of the ssreflect tactics, a brief - description of the mathematical components libraries - and a detailed list of the changes made in the releases - is available as an Inria Research Report at - - http://hal.inria.fr/inria-00258384 - - -AVAILABILITY -============ - - Ssreflect and the Mathematical Components library are available at: - http://math-comp.github.io/math-comp/ - - -THE DISCUSSION LIST -=================== - - The ssreflect list (ssreflect@msr-inria.inria.fr) is meant to be - a standard way to discuss about the ssreflect extension and the - mathematical components library. - - To subscribe visit: https://sympa.inria.fr/sympa/info/ssreflect - -LICENSING -========= - - This program is free software; you can redistribute it and/or modify - it under the terms of the CeCILL B FREE SOFTWARE LICENSE. - - You should have received a copy of the CeCILL B License with this - Kit, in the file named "CeCILL-B". - If not, visit http://www.cecill.info |