Merge pull request #18 from math-comp/prepare.1.1

Prepare next release

.travis.yml

@@ -1,14 +1,48 @@
 sudo: required
 dist: trusty
 language: coq
+cache:
+  apt: true
 branches:
   only:
   - master
-services:
-- docker
-before_install:
-- docker pull strubpy/coq:ssr-dev
+env:
+  global:
+  - NJOBS=2
+  # system is == 4.02.3
+  - COMPILER="system"
+  # Main test targets
+  matrix:
+  - COQ="8.6.1" MATHCOMP="1.6.1"
+  - COQ="8.6.1" MATHCOMP="1.7.0"
+  - COQ="8.7.2" MATHCOMP="1.7.0"
+  - COQ="8.8.1" MATHCOMP="1.7.0"
+  - COQ="8.8.1" MATHCOMP="dev"
+  - COQ="dev" MATHCOMP="1.7.0"
+  - COQ="dev" MATHCOMP="dev"
+matrix:
+  allow_failures:
+  - env: COQ="8.6.1" MATHCOMP="1.6.1"
+  fast_finish: true
+install:
+- sudo add-apt-repository --yes ppa:avsm/ppa
+- sudo apt-get update -qq
+- sudo apt-get install -qq -y opam
+- opam init -y
+- eval $(opam config env)
+- opam config var root
+- opam remote add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+- opam remote add coq-core-dev  https://coq.inria.fr/opam/core-dev
+- opam remote add coq-released  https://coq.inria.fr/opam/released
+- opam pin add -nvy coq --kind version ${COQ}
+- opam pin add -nvy coq-mathcomp-ssreflect --kind version ${MATHCOMP}
+- opam pin add -nvy .
+- |
+  # Building coq
+  travis_wait opam install -j ${NJOBS} -y ocamlfind camlp5 coq
+- |
+  # Building other deps
+  travis_wait opam install -j ${NJOBS} -y --deps-only coq-mathcomp-multinomials
+- opam list
 script:
-- >-
-  docker run -v $PWD:/home/ci/multinomials strubpy/coq:ssr-dev
-  sh -c 'cd multinomials && opam config exec -- make'
+- opam install -j ${NJOBS} -y -vvv coq-mathcomp-multinomials

Makefile

@@ -1,24 +1,8 @@
 # -*- Makefile -*-
 
 # --------------------------------------------------------------------
-NAME     := SsrMultinomials
-SUBDIRS  :=
-INCFLAGS := -R src $(NAME)
-COQFILES := \
-	src/xfinmap.v \
-	src/ssrcomplements.v \
-	src/monalg.v \
-	src/freeg.v \
-	src/mpoly.v
-
 include Makefile.common
 
-# --------------------------------------------------------------------
-.PHONY: install
-
-install:
-	$(MAKE) -f Makefile.coq install
-
 # --------------------------------------------------------------------
 this-clean::
 	rm -f *.glob *.d *.vo
@@ -39,6 +23,3 @@ dist:
 	BZIP2=-9 tar $(TAROPT) -cjf $(DISTDIR).tar.bz2 $(DISTDIR)
 	rm -rf $(DISTDIR)
 
-count:
-	@coqwc $(COQFILES) | tail -1 | \
-	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'

Makefile.common

@@ -1,51 +1,103 @@
 # -*- Makefile -*-
 
-# --------------------------------------------------------------------
+######################################################################
+# USAGE:                                                             #
+# The rules this-config::, this-build::, this-distclean::,           #
+# pre-makefile::, this-clean:: and __always__:: may be extended      #
+# Additionally, the following variables may be customized:           #
+SUBDIRS?=
+COQBIN?=$(dir $(shell which coqtop))
+COQMAKEFILE?=$(COQBIN)coq_makefile
+COQDEP?=$(COQBIN)coqdep
+COQPROJECT?=_CoqProject
+COQMAKEOPTIONS?=
+COQMAKEFILEOPTIONS?=
+V?=
+VERBOSE?=V
+######################################################################
+
+# local context: -----------------------------------------------------
 .PHONY: all config build clean distclean __always__
 .SUFFIXES:
 
-TOP     := $(dir $(lastword $(MAKEFILE_LIST)))
-COQMAKE := $(MAKE) -f Makefile.coq
-COQC    ?= $(COQBIN)coqc
+H:= $(if $(VERBOSE),,@)  # not used yet
+TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
+COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
+BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
+	     | wc -l | sed 's/ *//g')
 
-# --------------------------------------------------------------------
+# coq version:
+ifneq "$(BRANCH_coq)" "0"
+COQV:=dev
+COQVV:=dev
+COQVVV:=dev
+else
+COQV:= $(shell $(COQBIN)coqtop -v | head -1 \
+	     | sed 's/.*version \([0-9]\)[^ ]* .*/\1/')
+COQVV:= $(shell $(COQBIN)coqtop -v | head -1 \
+	     | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/\1/')
+COQVVV:= $(shell $(COQBIN)coqtop -v | head -1 \
+	     | sed 's/.*version \([0-9]\.[0-9]\.[0-9]\)[^ ]* .*/\1/')
+endif
+
+# all: ---------------------------------------------------------------
 all: config build
 
-# --------------------------------------------------------------------
-Makefile.coq: Makefile
-	coq_makefile $(INCFLAGS) $(COQFILES) -o Makefile.coq
-	-+$(COQMAKE) depend
+# Makefile.coq: ------------------------------------------------------
+.PHONY: pre-makefile
+
+Makefile.coq: pre-makefile $(COQPROJECT) Makefile
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
 
-# --------------------------------------------------------------------
-config: sub-config this-config Makefile.coq
+# Global config, build, clean and distclean --------------------------
+config: sub-config this-config
 
 build: sub-build this-build
 
 clean: sub-clean this-clean
 
 distclean: sub-distclean this-distclean
 
-# --------------------------------------------------------------------
+# Local config, build, clean and distclean ---------------------------
 .PHONY: this-config this-build this-distclean this-clean
 
-this-build::
+this-config:: __always__
+
+this-build:: this-config Makefile.coq
 	+$(COQMAKE)
 
 this-distclean:: this-clean
-	rm -f Makefile.coq
+	rm -f Makefile.coq Makefile.coq.conf Makefile.coq
+
+this-clean:: __always__
+	@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
+
+# Install target -----------------------------------------------------
+.PHONY: install
+
+install: __always__ Makefile.coq
+	$(COQMAKE) install
+# counting lines of Coq code -----------------------------------------
+.PHONY: count
+
+COQFILES = $(shell grep '.v$$' $(COQPROJECT))
 
-this-clean::
-	@if [ -f Makefile.coq ]; then $(COQMAKE) clean; fi
+count:
+	@coqwc $(COQFILES) | tail -1 | \
+	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
+# Additionally cleaning backup (*~) files ----------------------------
+this-distclean::
+	rm -f $(shell find . -name '*~')
 
-# --------------------------------------------------------------------
+# Make in SUBDIRS ----------------------------------------------------
 ifdef SUBDIRS
 sub-%: __always__
-	@set -e; for d in $(SUBDIRS); do $(MAKE) -C $$d $(@:sub-%=%); done
+	@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
 else
 sub-%: __always__
 	@true
 endif
 
-# --------------------------------------------------------------------
-%.vo: __always__
+# Make of individual .vo ---------------------------------------------
+%.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@

README.md

@@ -3,7 +3,7 @@
 A Coq/SSReflect Library for Monoidal Rings && Multinomials
 ========================================================================
 
-  This library is based on SSReflect/MathComp Library version 1.5/1.6.
+  This library is based on SSReflect/MathComp Library version >= 1.6.
 
   It can be installed from the unstable Coq opam repository:
 
@@ -22,5 +22,5 @@ Contributors:
 This library is also the result of discussions with:
 
   - Sophie Bernard
-  - [Cyril Cohen](http://perso.crans.org/cohen/)
+  - [Cyril Cohen](http://www.cyrilcohen.fr/)
   - [Laurence Rideau](http://www-sop.inria.fr/members/Laurence.Rideau/)

_CoqProject

@@ -0,0 +1,7 @@
+src/xfinmap.v
+src/ssrcomplements.v
+src/monalg.v
+src/freeg.v
+src/mpoly.v
+
+-R src SsrMultinomials

descr

@@ -0,0 +1 @@
+A Multivariate polynomial Library for the Mathematical Components Library.

opam

@@ -0,0 +1,31 @@
+opam-version: "1.2"
+name: "coq-mathcomp-multinomials"
+maintainer: "[email protected]"
+homepage: "https://github.com/math-comp/multinomials-ssr"
+bug-reports: "https://github.com/math-comp/multinomials-ssr/issues"
+dev-repo: "git+https://github.com/math-comp/multinomials.git"
+license: "CeCILL-B"
+authors: ["Pierre-Yves Strub"]
+build: [
+  [make "INSTMODE=global" "config"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+remove: ["rm" "-R" "%{lib}%/coq/user-contrib/SsrMultinomials"]
+depends: [
+  "coq" {(>= "8.5" | = "dev")}
+  "coq-mathcomp-ssreflect" { (>= "1.6" | = "dev") }
+  "coq-mathcomp-algebra"   { (>= "1.6" | = "dev") }
+  "coq-mathcomp-bigenough" {>= "1.0.0" & < "1.1.0~"}
+  "coq-mathcomp-finmap"    {>= "1.0.0" & < "1.1.0~"}
+]
+tags: [
+  "keyword:multinomials"
+  "keyword:monoid algebra"
+  "category:Math/Algebra/Multinomials"
+  "category:Math/Algebra/Monoid algebra"
+  "date:2016"
+  "logpath:SsrMultinomials"
+]

src/freeg.v

@@ -75,8 +75,6 @@ Module FreegDefs.
       _ : reduced seq_of_prefreeg
     }.
 
-    Implicit Arguments mkPrefreeg [].
-
     Local Coercion seq_of_prefreeg : prefreeg >-> seq.
 
     Lemma prefreeg_reduced: forall (D : prefreeg), reduced D.
@@ -95,7 +93,7 @@ Module FreegDefs.
     Canonical  prefreeg_choiceType  := Eval hnf in ChoiceType prefreeg prefreeg_choiceMixin.
   End Defs.
 
-  Implicit Arguments mkPrefreeg [G K].
+  Arguments mkPrefreeg [G K].
 
   Section Quotient.
     Variable G : zmodType.

src/mpoly.v

@@ -937,7 +937,7 @@ Proof. by rewrite mdeg0. Qed.
 End DegBoundMultinom.
 
 Definition bm0 n b := BMultinom (bm0_proof n b).
-Implicit Arguments bm0 [n b].
+Arguments bm0 [n b].
 
 Notation "''X_{1..' n  <  b '}'"       := (bmultinom n b).
 Notation "''X_{1..' n  <  b1 , b2 '}'" := ('X_{1..n < b1} * 'X_{1..n < b2})%type.
@@ -1641,7 +1641,7 @@ rewrite [X in _=X]big_uncond //= => j /memN_msupp_eq0.
 by move=> ->; rewrite mulr0 freegU0.
 Qed.
 
-Implicit Arguments mpoly_mulwE [p q].
+Arguments mpoly_mulwE [p q].
 
 Lemma mpoly_mul_revwE p q kp kq : msize p <= kp -> msize q <= kq ->
   p *M q = [mpoly \sum_(m : 'X_{1..n < kq, kp}) (p *M_[(m.2, m.1)] q)].
@@ -1650,7 +1650,7 @@ move=> lep leq;  rewrite -pair_bigA_curry exchange_big /=.
 by rewrite pair_bigA /= -mpoly_mulwE //.
 Qed.
 
-Implicit Arguments mpoly_mul_revwE [p q].
+Arguments mpoly_mul_revwE [p q].
 
 Lemma mcoeff_poly_mul p q m k : !|m| < k ->
   (p *M q)@_m =
@@ -1713,7 +1713,7 @@ rewrite -(pair_big_dep xpredT P F) (bigID Q) /= addrC.
   move/mnmP/(_ i); rewrite mnmDE=> eq; move: Nle.
   by rewrite eq leq_addr.
 Qed.
-Implicit Arguments mcoeff_poly_mul_lin [p q m].
+Arguments mcoeff_poly_mul_lin [p q m].
 
 Local Notation mcoeff_pml := mcoeff_poly_mul_lin.
 
@@ -1736,7 +1736,7 @@ rewrite ltn_neqAle -subn_eq0 => /andP [ne_mhi /eqP le_mhi].
 apply/negbTE/eqP/mnmP=> /(_ i); rewrite !mnmBE => /eqP.
 by rewrite le_mhi subn0 (negbTE ne_mhi).
 Qed.
-Implicit Arguments mcoeff_poly_mul_lin_rev [p q m].
+Arguments mcoeff_poly_mul_lin_rev [p q m].
 
 Local Notation mcoeff_pmlr := mcoeff_poly_mul_lin_rev.
 
@@ -2619,7 +2619,7 @@ move=> le_pk; rewrite /mderiv (big_mksub I) /=; first last.
 rewrite big_uncond //= => j /memN_msupp_eq0 ->.
 by rewrite mulr0 scale0r.
 Qed.
-Implicit Arguments mderivwE [p i].
+Arguments mderivwE [i p].
 
 Lemma mcoeff_deriv i m p : p^`M(i)@_m = p@_(m + U_(i)) *+ (m i).+1.
 Proof.
@@ -3006,7 +3006,7 @@ rewrite /mmap (big_mksub I) ?msupp_uniq //=; first last.
 rewrite big_uncond //= => j /memN_msupp_eq0 ->.
 by rewrite raddf0 mul0r.
 Qed.
-Implicit Arguments mmapE [p].
+Arguments mmapE [p].
 
 Lemma mmap_is_additive : additive (mmap f h).
 Proof.
@@ -3035,7 +3035,7 @@ by rewrite mcoeffC eqxx mulr1.
 Qed.
 End Additive.
 
-Implicit Arguments mmapE [f h p].
+Arguments mmapE [h f p].
 
 Section Multiplicative.
 Variable h : 'I_n -> S.
@@ -3070,7 +3070,7 @@ Qed.
 End Multiplicative.
 End MPolyMorphism.
 
-Implicit Arguments mmapE [n R S h f p].
+Arguments mmapE [n R S h f p].
 
 (* -------------------------------------------------------------------- *)
 Lemma mmap1_eq n (R : ringType) (f1 f2 : 'I_n -> R) m :
@@ -3328,7 +3328,7 @@ Proof.
 rewrite /map_mpoly; move/mmapE=> -> /=; apply/eq_bigr.
 by move=> i _; rewrite mmap1_id mul_mpolyC.
 Qed.
-Implicit Arguments map_mpolyE [p].
+Arguments map_mpolyE [p].
 
 Lemma mcoeff_map_mpoly m p : p^f@_m = f p@_m.
 Proof.
@@ -3688,7 +3688,7 @@ rewrite [X in _='X_[X]](reindex (fun i : 'I_n => s i)) /=.
 by exists (s^-1)%g=> i _; rewrite (permK, permKV).
 Qed.
 
-Implicit Arguments msymE [p].
+Arguments msymE [p].
 
 Lemma mcoeff_sym p (s : 'S_n) m : (msym s p)@_m = p@_(m#s).
 Proof.
@@ -3842,8 +3842,8 @@ by move/msupp_le_mlead; rewrite leNgt => /negbTE=> ->.
 Qed.
 End MPolySym.
 
-Implicit Arguments inj_msym [n R].
-Implicit Arguments symmetric [n R].
+Arguments inj_msym [n R].
+Arguments symmetric [n R].
 
 (* -------------------------------------------------------------------- *)
 Section MPolySymComp.