Skip to content

Commit

Permalink
Nouvelle version de CoRN, qui:
Browse files Browse the repository at this point in the history 
 - compile avec Coq trunk du 31 Mars 2006 (et non de mi-juin 2006)
 - ajoute de nouveaux développements:
   * nshmyrev contribution: reals aren't countable and more
 - n'utilise plus de code ML (toutes les tactiques en LTac)
 - tactique Algebra renommée en algebra pour plus d'uniformité avec
   les tactiques de Coq.
 - Compile avec gcc récent
Au passage, zappe les informations de licence.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq-contribs/trunk/Nijmegen/CoRN@454 0cf17b13-060f-0410-b1b1-c666bec9822a
  • Loading branch information
lmamane committed Jun 15, 2006
1 parent e04615f commit 7ce488e
Show file tree
Hide file tree
Showing 191 changed files with 3,781 additions and 4,962 deletions.
6 changes: 0 additions & 6 deletions .cvsignore
View file

This file was deleted.

504 changes: 0 additions & 504 deletions LICENSE
View file

This file was deleted.

34 changes: 18 additions & 16 deletions Makefile.common
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ endif
SHELL:=bash -O nullglob

# realpath utility to use
REALPATH := $(shell if ! which realpath 2>/dev/null; then $(MAKE) -f "$(SRCDIR)/Makefile.realpath" -s TOPDIR="$(TOPDIR)" realpath; echo "$(SRCDIR)/bin/realpath"; fi)
REALPATH := $(shell if ! type -p realpath 2>/dev/null; then $(MAKE) -f "$(SRCDIR)/Makefile.realpath" -s TOPDIR="$(TOPDIR)" realpath; echo "$(SRCDIR)/bin/realpath"; fi)

SRCDIR:=$(shell "$(REALPATH)" "$(SRCDIR)")

Expand Down Expand Up @@ -68,9 +68,10 @@ GLOBFILE = $(SRCDIR)/.glob
## End of user-configurable variables
## Please don't edit beyond this line, unless you really know what you are doing

# Various executables we build
# Various executables we build when we need a custom Coq image.
# (Thus currently not.)
TOPLEVEL := $(LIBDIR)/$(TOPLEVELNAME)
BINARIES:=$(BINDIR)/$(TOPLEVELNAME) $(BINDIR)/$(COMPILERNAME)
BINARIES:=$(BINDIR)/$(TOPLEVELNAME) $(BINDIR)/$(COMPILERNAME) $(BINDIR)/$(IDENAME)
LIBEXECS:=$(LIBDIR)/$(TOPLEVELNAME) $(LIBDIR)/$(COMPILERNAME)
IDELIB:=$(LIBDIR)/$(IDENAME)
IDEBIN:=$(BINDIR)/$(IDENAME)
Expand Down Expand Up @@ -98,6 +99,7 @@ COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
-I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \
-I $(CAMLP4LIB)
COQC := $(COQBIN)/coqc
COQIDE := $(COQBIN)/coqide
COQDEP := $(COQBIN)/coqdep
COQMKTOP := $(COQBIN)/coqmktop
GRAMMARS:=grammar.cma
Expand All @@ -107,7 +109,7 @@ PP:=-pp "camlp4o -I $(SRCDIR)/tactics -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRA
COQMAP = -R $(SRCDIR) $(LIBNAME)
OTHERFLAGS = -dump-glob $(GLOBFILE) -I $(SRCDIR)/tactics $(COQMAP)
COQFLAGS = $(COQ_XML) $(OPT) $(OTHERFLAGS)
COQCFLAGS = -image $(TOPLEVEL)
COQCFLAGS =
COQDOCFLAGS = --toc -s -t "C-CoRN Documentation" $(COQMAP) \
--glob-from $(GLOBFILE) -g -l --multi-index --files-from $(DOCLIST)
COQDEPFLAGS := $(shell echo $(COQDIRS) | awk -v RS=' ' -v ORS=' ' -v pwd="`pwd`" '{ if ( $$1 != pwd ) print "-I " $$1}')
Expand All @@ -123,7 +125,7 @@ ifdef CoRN_MF_sub
all : $(COQOBJECTS)
else
all :
$(MAKE) CoRN_MF_sub=1 all
exec $(MAKE) CoRN_MF_sub=1 all
endif

# Convenience utilities for humans
Expand All @@ -137,7 +139,7 @@ makefiles : $(AUTO_MAKEFILES)

$(AUTO_MAKEFILES) :
@set -e; if ! [ -a $@ ]; then \
depth="`echo -n "$(patsubst $(SRCDIR)/%,%,$@)" | sed 's|[^/]||g' | wc -c | sed 's|[[:space:]]||g'`"; \
depth=$$(echo '$(patsubst $(SRCDIR)/%,%,$@)' | awk '{ print gsub("/","/") }'); \
model="$(SRCDIR)/Makefile.auto.$${depth}"; \
if ! [ -a "$${model}" ]; then \
( echo -n 'TOPDIR=..'; i=1; \
Expand Down Expand Up @@ -167,36 +169,36 @@ $(IDELIB): $(CMX) | $(LIBDIR)
@echo Building coq-ide top-level $(subst $(SRCDIR)/,, $@)
@$(COQMKTOP) -ide -srcdir $(COQTOP) -ide -opt -o $@ $(CMX)

$(IDEBIN): | $(BINDIR) $(IDELIB)
$(IDEBIN): | $(BINDIR)
@echo Building coq-ide top-level startup script
@set -e; ( \
echo '#!/bin/sh'; \
echo 'exec $(LIBDIR)/$(IDENAME) $(COQFLAGS) $$*' \
echo 'exec "$(COQIDE)" $(COQFLAGS) "$$@"' \
) > $@; chmod +x $@

$(LIBDIR)/$(TOPLEVELNAME): $(CMX) | $(LIBDIR)
@echo Building top-level $(subst $(SRCDIR)/,,$@)
@$(COQMKTOP) -srcdir $(COQTOP) -opt -o $@ $(CMX)

$(BINDIR)/$(TOPLEVELNAME): | $(BINDIR) $(LIBDIR)/$(TOPLEVELNAME)
$(BINDIR)/$(TOPLEVELNAME): | $(BINDIR)
@echo Building top-level startup script
@set -e; ( \
echo '#!/bin/sh'; \
echo 'exec $(TOPLEVEL) $(COQFLAGS) $$*' \
echo 'exec "$(COQBIN)/coqtop" $(COQFLAGS) "$$@"' \
) > $@; chmod +x $@

$(LIBDIR)/$(COMPILERNAME): | $(LIBDIR) $(LIBDIR)/$(TOPLEVELNAME)
@echo Building compiler $(subst $(SRCDIR)/,, $@)
@set -e; ( \
echo '#!/bin/sh'; \
echo 'exec $(COQC) $(COQCFLAGS) $$*' \
echo 'exec $(COQC) $(COQCFLAGS) "$$@"' \
) > $@; chmod +x $@

$(BINDIR)/$(COMPILERNAME): | $(BINDIR) $(LIBDIR)/$(COMPILERNAME)
$(BINDIR)/$(COMPILERNAME): | $(BINDIR)
@echo Building compiler startup script
@set -e; ( \
echo '#!/bin/sh'; \
echo 'exec $(LIBDIR)/$(COMPILERNAME) $(COQFLAGS) $$*' \
echo 'exec "$(COQC)" $(COQFLAGS) "$$@"' \
) > $@; chmod +x $@

%.cmx : %.ml
Expand All @@ -208,10 +210,10 @@ $(BINDIR)/$(COMPILERNAME): | $(BINDIR) $(LIBDIR)/$(COMPILERNAME)
@$(OCAMLC) -c $(COQSRC) $(PP) $<

ifdef CoRN_MF_sub
%.vo : %.v $(TOPLEVEL)
%.vo : %.v
@set -e; \
echo "Compiling $<"; \
$(COQC) $(COQFLAGS) $(COQCFLAGS) $<
exec $(COQC) $(COQFLAGS) $(COQCFLAGS) $<
else
.PHONY: always

Expand All @@ -226,7 +228,7 @@ else
fi \
}; \
canon_name="$$(canonicalise "$@")" ; \
$(MAKE) CoRN_MF_sub=1 "$${canon_name}"
exec $(MAKE) CoRN_MF_sub=1 "$${canon_name}"
endif

dep : $(DEPEND) $(DOCDEPEND)
Expand Down
1 change: 1 addition & 0 deletions Makefile.realpath
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

SRCDIR=$(shell pwd)/$(TOPDIR)
BINDIR=$(SRCDIR)/bin
CFLAGS:=-O3 -DVERSION='"1.9.25"' $(CFLAGS)

.PHONY : realpath clean

Expand Down
30 changes: 19 additions & 11 deletions README
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,20 +11,25 @@ A (no longer updated) version compatible with version 7.4 is also
available.

Before installing C-CoRN, please check that you have:
- Coq version 8.0 (a compiled source tree, not only a binary package)
- the OCaml you used to compile Coq
- Coq version 8.0
(CoRN used to require a compiled source tree, but a binary package will
do these days.)
- at least 128MiB RAM memory available (and preferably more, especially if
you plan to use the formalization of Real Analysis).
- GNU make version 3.80 or later
- a POSIX-compliant operating system. This means Unix, a clone
thereof or a good emulation layer on top of another OS. In
particular, *hard* links must be supported by the file system.
- the GNU Bourne Again SHell (we use some bashisms)
- At least one of:
* The "realpath" utility in your PATH (Debian package realpath).
* A C compiler.

In order for C-CoRN to work, you need to set some environment variables.
We advise you to do this inside a .bash_profile or similar.
- COQTOP should be set to the location of the Coq sources (e.g.
/usr/local/src/coq-8.0/)
- COQTOP should be set to the Coq installation prefix (e.g. /usr/ or
/usr/local/) or the location of a compiled Coq source tree (e.g.
/usr/local/src/coq-8.0/).
- COQBIN should be set to the directory where the Coq binaries can
be found, if different from ${COQTOP}/bin/.

Expand Down Expand Up @@ -113,23 +118,26 @@ are recognized.
OCAMLC=file
OCAMLOPT=file
-> Choose an ocamlc and ocamlopt to use
(Obsolete, as CoRN does not use OCaml anymore.)
COQDOC=file -> Choose a coqdoc to use

HUMAN CONVENIENCE
-----------------

CoRN now has a few facilities for the convenience of the human beings
using it. Enable with "make human", or "make ide" for coqide support
(this needs a coqide-enabled Coq).
using it. Enable with "make human".

This will create Makefiles in every directory scanned for .v files
(but will not overwrite the Makefile if any is present) so that all
make commands work from anywhere in the CoRN hierarchy.

It also populates the "bin" directory with CoRNc, CoRNtop and (with
coqide support) CoRNide. These are CoRN versions of coqc, coqtop and
coqide, respectively. We suggest you add the "bin" directory of CoRN
to your PATH.
It also populates the "bin" directory with CoRNc, CoRNtop and
CoRNide. These are CoRN versions of coqc, coqtop and coqide,
respectively. We suggest you add the "bin" directory of CoRN to your
PATH.

The old "ide" target is obsolete, as CoRN does not require a custom
Coq image anymore.

DEPENDENCIES
------------
Expand All @@ -147,5 +155,5 @@ For any questions, comments, bug reports or other feel free to e-mail
lcf@cs.kun.nl.

$Id$

LocalWords: Nijmegen CoRN Coq CVS
16 changes: 0 additions & 16 deletions algebra/Basics.v
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,3 @@
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)


(* $Id$ *)

(** printing alpha %\ensuremath{\alpha}% #&alpha;# *)
Expand Down
50 changes: 17 additions & 33 deletions algebra/CAbGroups.v
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,3 @@
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)


Require Export CGroups.

Section Abelian_Groups.
Expand Down Expand Up @@ -253,50 +237,50 @@ Fixpoint nmult (a:G) (n:nat) {struct n} : G :=

Lemma nmult_wd : forall (x y:G) (n m:nat), (x [=] y) -> n = m -> nmult x n [=] nmult y m.
simple induction n; intros.
rewrite <- H0; Algebra.
rewrite <- H1; simpl in |- *; Algebra.
rewrite <- H0; algebra.
rewrite <- H1; simpl in |- *; algebra.
Qed.

Lemma nmult_one : forall x:G, nmult x 1 [=] x.
simpl in |- *; Algebra.
simpl in |- *; algebra.
Qed.

Lemma nmult_Zero : forall n:nat, nmult Zero n [=] Zero.
intro n.
induction n.
Algebra.
algebra.
simpl in |- *; Step_final ((Zero:G)[+]Zero).
Qed.

Lemma nmult_plus : forall m n x, nmult x m[+]nmult x n [=] nmult x (m + n).
simple induction m.
simpl in |- *; Algebra.
simpl in |- *; algebra.
clear m; intro m.
intros.
simpl in |- *. Step_final (x[+](nmult x m[+]nmult x n)).
Qed.

Lemma nmult_mult : forall n m x, nmult (nmult x m) n [=] nmult x (m * n).
simple induction n.
intro. rewrite mult_0_r. Algebra.
intro. rewrite mult_0_r. algebra.
clear n; intros.
simpl in |- *.
rewrite mult_comm. simpl in |- *.
eapply eq_transitive_unfolded.
2: apply nmult_plus.
rewrite mult_comm. Algebra.
rewrite mult_comm. algebra.
Qed.

Lemma nmult_inv : forall n x, nmult [--]x n [=] [--] (nmult x n).
intro; induction n; simpl in |- *.
Algebra.
algebra.
intros.
Step_final ([--]x[+] [--](nmult x n)).
Qed.

Lemma nmult_plus' : forall n x y, nmult x n[+]nmult y n [=] nmult (x[+]y) n.
intro; induction n; simpl in |- *; intros.
Algebra.
algebra.
astepr (x[+]y[+](nmult x n[+]nmult y n)).
astepr (x[+](y[+](nmult x n[+]nmult y n))).
astepr (x[+](y[+]nmult x n[+]nmult y n)).
Expand Down Expand Up @@ -336,7 +320,7 @@ astepl (nmult x (nat_of_P p)).
apply cg_cancel_rht with (nmult x n).
astepr (nmult x m).
astepl (nmult x (nat_of_P p + n)).
apply nmult_wd; Algebra.
apply nmult_wd; algebra.
rewrite <- convert_is_POS in H.
auto with zarith.

Expand All @@ -351,15 +335,15 @@ astepr (nmult x m[+] [--](nmult x m)[+]nmult x n).
astepr (Zero[+]nmult x n).
astepr (nmult x n).
astepl (nmult x (m + nat_of_P p)).
apply nmult_wd; Algebra.
apply nmult_wd; algebra.
rewrite <- min_convert_is_NEG in H.
auto with zarith.
Qed.

Lemma zmult_wd : forall (x y:G) (n m:Z), (x [=] y) -> n = m -> zmult x n [=] zmult y m.
do 3 intro.
case n; intros; inversion H0.
Algebra.
algebra.
unfold zmult in |- *.
simpl in |- *.
astepl (nmult x (nat_of_P p)); Step_final (nmult y (nat_of_P p)).
Expand All @@ -369,20 +353,20 @@ Step_final [--](nmult y (nat_of_P p)).
Qed.

Lemma zmult_one : forall x:G, zmult x 1 [=] x.
simpl in |- *; Algebra.
simpl in |- *; algebra.
Qed.

Lemma zmult_min_one : forall x:G, zmult x (-1) [=] [--]x.
intros; simpl in |- *; Step_final (Zero[-]x).
Qed.

Lemma zmult_zero : forall x:G, zmult x 0 [=] Zero.
simpl in |- *; Algebra.
simpl in |- *; algebra.
Qed.

Lemma zmult_Zero : forall k:Z, zmult Zero k [=] Zero.
intro; induction k; simpl in |- *.
Algebra.
algebra.
Step_final ((Zero:G)[-]Zero).
Step_final ((Zero:G)[-]Zero).
Qed.
Expand Down Expand Up @@ -442,7 +426,7 @@ Step_final (nmult Zero (nat_of_P p)).
astepr [--](Zero:G). astepl [--](nmult (Zero[-]Zero) (nat_of_P p)).
Step_final [--](nmult Zero (nat_of_P p)).

Algebra.
algebra.

astepr (nmult x (nat_of_P (p * p0))).
astepl (nmult (nmult x (nat_of_P p)) (nat_of_P p0)[-]Zero).
Expand All @@ -454,7 +438,7 @@ astepl (Zero[-]nmult (nmult x (nat_of_P p)) (nat_of_P p0)).
astepl [--](nmult (nmult x (nat_of_P p)) (nat_of_P p0)).
rewrite nat_of_P_mult_morphism. apply un_op_wd_unfolded. apply nmult_mult.

Algebra.
algebra.

astepr [--](nmult x (nat_of_P (p * p0))).
astepl (nmult [--](nmult x (nat_of_P p)) (nat_of_P p0)[-]Zero).
Expand Down
16 changes: 0 additions & 16 deletions algebra/CAbMonoids.v
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,3 @@
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)


Require Export CMonoids.

Section Abelian_Monoids.
Expand Down
Loading

0 comments on commit 7ce488e

Please sign in to comment.