Moving to coq 8.10 and dune build

.gitignore

@@ -18,6 +18,10 @@
 *.dko
 *.tar.bz2
 
+# dune files.
+_build/
+
+
 summary.csv
 
 run/main/**/*.dk

.travis.yml

@@ -15,9 +15,9 @@ cache:
 env:
   global:
   - OPAMJOBS="2"
-  - OPAMYES="true"
-  - OPAMVERBOSE="true"
-  - OCAML_VERSION=4.06.0
+  - OPAMYES=1
+  - OPAMVERBOSE=1
+  - OCAML_VERSION=4.09.0
 
 before_install:
   # Obtain and install opam locally.
@@ -26,8 +26,8 @@ before_install:
   # Initialize the switch.
   - opam init -a --disable-sandboxing --compiler="$OCAML_VERSION"
   - opam update
-  - opam switch "$OCAML_VERSION"
-  - eval $(opam env)
+  - opam switch ${OCAML_VERSION} || opam switch create ${OCAML_VERSION}
+  - eval `opam config env`
   - opam pin add dedukti https://github.com/Deducteam/Dedukti.git#acu-state
   - opam install dedukti
   - opam pin add --no-action coqine .
@@ -38,8 +38,6 @@ install:
 
 script:
   - make plugin
-  - echo "Add ML Path \"$(pwd)/src\"." >> $HOME/.coqrc
-  - cat $HOME/.coqrc
   - make -C encodings
   - make
   - make tests

Makefile

@@ -1,16 +1,17 @@
+# Compile with "make Q=" to display the commands that are run.
+Q = @
+
 # Variables
 COQ_MAKEFILE ?= coq_makefile
 COQTOP       ?= coqtop
 DKCHECK      ?= dkcheck
 DKDEP        ?= dkdep
 VERBOSE      ?=
 
-CAMLFLAGS="-bin-annot -annot"
-
 RUNDIR=run
 
 COQ_VERSION   := $(shell $(COQTOP) -print-version)
-CHECK_VERSION := $(shell $(COQTOP) -print-version | grep "8\.8\.*")
+CHECK_VERSION := $(shell $(COQTOP) -print-version | grep "8\.10\.*")
 
 define MANUAL
 
@@ -95,25 +96,25 @@ check-version:
 ifeq ("$(CHECK_VERSION)","")
 	$(warning "Incorrect Coq version !")
 	$(warning "Found: $(COQ_VERSION).")
-	$(warning "Expected: 8.8.x")
+	$(warning "Expected: 8.1°.x")
 	$(error "To ignore this, use:  make CHECK_VERSION=ignore")
 endif
 
-plugin: CoqMakefile
-	make -f CoqMakefile VERBOSE=$(VERBOSE) - all
+plugin:
+	$(Q)dune build
 
-install: CoqMakefile plugin
-	make -f CoqMakefile - install
+doc:
+	$(Q)dune build @doc
 
-uninstall: CoqMakefile
-	make -f CoqMakefile - uninstall
+install: all
+	$(Q)dune install
 
-.merlin: CoqMakefile
-	make -f CoqMakefile .merlin
+uninstall: all
+	$(Q)dune uninstall
 
-clean: CoqMakefile
+clean:
+	$(Q)dune clean
 	make -C encodings - clean
-	make -f CoqMakefile - clean
 
 	make -C $(RUNDIR)/main            clean
 	make -C $(RUNDIR)/mathcomp        clean
@@ -129,18 +130,21 @@ clean: CoqMakefile
 	rm -f $(RUNDIR)/mathcomp/config.v
 	rm -f $(RUNDIR)/logipedia/config.v
 	rm -f $(RUNDIR)/upoly_logipedia/config.v
-	rm -f CoqMakefile
 	rm -f *.tar.bz2
 	rm -f summary.csv
 
 fullclean: clean
-	rm src/*.cmt
-	rm src/*.cmti
-	rm src/*.annot
-
-CoqMakefile: Make
-	$(COQ_MAKEFILE) -f Make -o CoqMakefile
-	echo "COQMF_CAMLFLAGS+=-annot -bin-annot -g" >> CoqMakefile.conf
+	rm -f src/*.annot
+	rm -f src/*.cmo
+	rm -f src/*.cma
+	rm -f src/*.cmi
+	rm -f src/*.cmt
+	rm -f src/*.cmti
+	rm -f src/*.a
+	rm -f src/*.o
+	rm -f src/*.cmx
+	rm -f src/*.cmxs
+	rm -f src/*.cmxa
 
 .coqrc: plugin
 	echo "Add ML Path \"$(shell pwd)/src\"." > .coqrc

coqine.opam

@@ -0,0 +1,16 @@
+synopsis:     "Coqine Plugin"
+description:  "Coqine Plugin"
+name:         "coqine"
+opam-version: "2.0"
+maintainer:   "[email protected]"
+authors:      "Gaspard FEREY"
+homepage:     "https://github.com/Deducteam/CoqInE/"
+bug-reports:  "https://github.com/Deducteam/CoqInE/"
+dev-repo:     "git+https://github.com/Deducteam/CoqInE"
+license:      "GPL 3"
+depends: [
+  "ocaml"         { >= "4.09.0"           }
+  "coq"           { = "8.10.0" }
+  "dune"          { build & >= "1.9.0"    }
+]
+build: [ "dune" "build" "-p" name "-j" jobs ]

dune-project

@@ -0,0 +1,3 @@
+(lang dune 1.9)
+(using coq 0.1)
+(name coqine)

encodings/theories/f_matita.dk

@@ -22,6 +22,7 @@ def max : Nat -> Nat -> Nat.
 [i,j] max (s i) (s j) --> s (max i j).
 
 (;
+Coqine sprop = prop
 Coqine prop  = prop
 Coqine type  = type
 Coqine set   = set

encodings/theories/fpredicates.dk

@@ -25,6 +25,7 @@ def max : Nat -> Nat -> Nat.
 [i,j] max (s i) (s j) --> s (max i j).
 
 (;
+Coqine sprop = prop
 Coqine prop  = prop
 Coqine type  = type
 Coqine set   = set

encodings/theories/functional.dk

@@ -23,6 +23,7 @@ def set   : Sort := type z.
 def type0 : Sort := type (s z).
 
 (;
+Coqine sprop = prop
 Coqine prop  = prop
 Coqine type  = type
 Coqine set   = set

encodings/theories/lift-predicates.dk

@@ -22,6 +22,7 @@ def max : Nat -> Nat -> Nat.
 [i,j] max (s i) (s j) --> s (max i j).
 
 (;
+Coqine sprop = prop
 Coqine prop  = prop
 Coqine type  = type
 Coqine set   = set

encodings/theories/original.dk

@@ -23,6 +23,7 @@ set  : Sort.
 type : Nat -> Sort.
 
 (;
+Coqine sprop = prop
 Coqine prop = prop
 Coqine set = set
 Coqine type = type

encodings/theories/predicates.dk

@@ -25,6 +25,7 @@ def max : Nat -> Nat -> Nat.
 [i,j] max (s i) (s j) --> s (max i j).
 
 (;
+Coqine sprop = prop
 Coqine prop  = prop
 Coqine type  = type
 Coqine set   = set

encodings/theories/predicates_ac.dk

@@ -24,6 +24,7 @@ def set   : Sort := type z.
 def type0 : Sort := type (s z).
 
 (;
+Coqine sprop = prop
 Coqine prop  = prop
 Coqine type  = type
 Coqine set   = set

run/logipedia/Makefile

@@ -2,14 +2,15 @@
 
 # Variables
 COQ_MAKEFILE ?= coq_makefile
-COQC         ?= coqc
+COQC         ?= coqc -allow-sprop
 DKCHECK      ?= dkcheck
 DKDEP        ?= dkdep
 VERBOSE      ?=
 MAINFILE     ?= main
 
 OUTFOLDER = out
-COQINEPATH=../../src
+COQINE_SRC=../../src/
+COQINE_LIB=../../_build/install/default/lib/coqine/plugin/
 
 DKS = $(wildcard $(OUTFOLDER)/*.dk)
 DKOS = $(DKS:.dk=.dko)
@@ -33,7 +34,7 @@ $(OUTFOLDER):
 
 # Generate the [.dk] files by executing [main_???.v]
 generate: compile $(OUTFOLDER)
-	$(COQC) -nois -init-file ../../.coqrc -verbose -R . Top $(MAINFILE).v
+	$(COQC) -nois -verbose -R . Top -Q $(COQINE_SRC) Coqine -I $(COQINE_LIB) $(MAINFILE).v
 
 # Generate the dependencies of [.dk] files
 depend:

run/main/Makefile

@@ -2,14 +2,15 @@
 
 # Variables
 COQ_MAKEFILE ?= coq_makefile
-COQC         ?= coqc
+COQC         ?= coqc -allow-sprop
 DKCHECK      ?= dkcheck
 DKDEP        ?= dkdep
 VERBOSE      ?=
 MAINFILE     ?= main_debug
 
 OUTFOLDER = out
-COQINEPATH=../../src
+COQINE_SRC=../../src/
+COQINE_LIB=../../_build/install/default/lib/coqine/plugin/
 
 DKS = $(wildcard $(OUTFOLDER)/*.dk)
 DKOS = $(DKS:.dk=.dko)
@@ -33,7 +34,7 @@ $(OUTFOLDER):
 
 # Generate the [.dk] files by executing [main_???.v]
 generate: compile $(OUTFOLDER)
-	$(COQC) -nois -init-file ../../.coqrc -verbose -R . Top $(MAINFILE).v
+	$(COQC) -nois -verbose -R . Top -Q $(COQINE_SRC) Coqine -I $(COQINE_LIB) $(MAINFILE).v
 
 # Generate the dependencies of [.dk] files
 depend:

run/main/Test/Debug.v

@@ -198,7 +198,8 @@ Section Defs.
   (** Any [Equivalence] declared in the context is automatically considered
    a rewrite crelation. *)
 
-  Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA.
+    Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA.
+    Defined.
 
   (** Leibniz equality. *)
   Section Leibniz.
@@ -216,8 +217,8 @@ Section Defs.
 End Defs.
 
 (** Default rewrite crelations handled by [setoid_rewrite]. *)
-Instance: RewriteRelation impl.
-Instance: RewriteRelation iff.
+Instance: RewriteRelation impl. Defined.
+Instance: RewriteRelation iff.  Defined.
 
 (** Hints to drive the typeclass resolution avoiding loops
  due to the use of full unification. *)
@@ -320,7 +321,7 @@ Section Binary.
   Definition relation_equivalence : crelation (crelation A) :=
     fun R R' => forall x y, iffT (R x y) (R' x y).
 
-  Global Instance: RewriteRelation relation_equivalence.
+  Global Instance: RewriteRelation relation_equivalence. Defined.
 
   Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
     fun x y => prod (R x y) (R' x y).

run/main/Test/Fixpoints.v

@@ -1,13 +1,39 @@
+
 Inductive nat :=
 | o : nat
 | s : nat -> nat.
 
+Definition plus_nat : nat -> nat -> nat :=
+  fun n =>
+    (
+      fix aux (m:nat) {struct m} : nat
+      := match m with
+         | o => n
+         | s m' => s (aux m') end
+    ).
+
+Definition even : nat -> bool :=
+  (fix even' (n:nat) : bool
+   :=
+     (match n with
+       o    => true
+     | s n' => odd' n'
+     end)
+   with odd' (n:nat) : bool
+   :=
+     (match n with
+       o    => false
+     | s n' => even' n'
+     end)
+   for even').
+
 Fixpoint id x :=
 match x with
 | o => o
 | s x => s (id x)
 end.
 
+
 Fixpoint id1 a b n :=
 match n with
 | o => a
@@ -32,6 +58,17 @@ Fixpoint f x :=
   end) x.
 
 
+Fixpoint f' x :=
+  match x with
+  | o => o
+  | s x1 => g' x1
+  end
+with g' y :=
+  match y with
+  | o => o
+  | s y1 => f' y1
+  end.
+
 
 Inductive nat' : Type :=
 | Z' : nat'

run/main/Test/Test.v

@@ -3,9 +3,14 @@ Inductive list {A:Type} : Type :=
 | Nil : list
 | Cons : A -> list -> list.
 
-Definition f : nat -> nat :=
+Definition g : nat -> nat :=
   fun x => (fix aux (n:nat) : nat := 0) x.
 
+Definition f : nat -> nat :=
+  fix  f (n:nat) {struct n} : nat := match n with 0 => 0 | S n' => S (g n') end
+  with g (n:nat) {struct n} : nat := n
+  for f.
+
 (*
 Eval compute in (fun x => f x).
  *)

run/main/import_debug.v

@@ -29,10 +29,11 @@ Fixpoint A m := fix A_m n :=
 
 Definition t'' := A 2 2.
 
+Set Allow StrictProp.
+
 Require Import
   Test.Test
   Test.Identity
-  Coq.Classes.RelationClasses
   Test.Polymorph
   Test.ImportA
   Test.ImportB
@@ -46,11 +47,17 @@ Require Import
   Test.Functors
   Test.NestedLibraries
   Test.Reflexivity
+(*
+  Test.Debuglib
+*)
+.
+
 
+Require Import
+  Coq.Classes.RelationClasses
 (*
 
   Coq.Arith.PeanoNat
-  Test.Debuglib
 
   Coq.Logic.Berardi
   Coq.Logic.ChoiceFacts