diff --git a/.travis.yml b/.travis.yml index 503f4fd..c002606 100644 --- a/.travis.yml +++ b/.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 diff --git a/Makefile b/Makefile index 30cdd26..0f8d48e 100644 --- a/Makefile +++ b/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)}' diff --git a/Makefile.common b/Makefile.common index 82df9fd..71b3192 100644 --- a/Makefile.common +++ b/Makefile.common @@ -1,23 +1,56 @@ # -*- 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 @@ -25,27 +58,46 @@ 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) $@ diff --git a/README.md b/README.md index 5da7833..7c08a14 100644 --- a/README.md +++ b/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/) diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..91f8d02 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,7 @@ +src/xfinmap.v +src/ssrcomplements.v +src/monalg.v +src/freeg.v +src/mpoly.v + +-R src SsrMultinomials \ No newline at end of file diff --git a/descr b/descr new file mode 100644 index 0000000..c708bb6 --- /dev/null +++ b/descr @@ -0,0 +1 @@ +A Multivariate polynomial Library for the Mathematical Components Library. diff --git a/opam b/opam new file mode 100644 index 0000000..cfbeb7f --- /dev/null +++ b/opam @@ -0,0 +1,31 @@ +opam-version: "1.2" +name: "coq-mathcomp-multinomials" +maintainer: "pierre-yves@strub.nu" +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" +] diff --git a/src/freeg.v b/src/freeg.v index 450a41e..62a23b3 100644 --- a/src/freeg.v +++ b/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. diff --git a/src/mpoly.v b/src/mpoly.v index a3bc755..7259b88 100644 --- a/src/mpoly.v +++ b/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. diff --git a/src/ssrcomplements.v b/src/ssrcomplements.v index 3afd27e..3eaa1d4 100644 --- a/src/ssrcomplements.v +++ b/src/ssrcomplements.v @@ -246,8 +246,8 @@ Section BigMkSub. Qed. End BigMkSub. -Implicit Arguments big_sub_widen [S idx op T sT rT]. -Implicit Arguments big_sub_widen [S idx op T sT rT]. +Arguments big_sub_widen [S idx op T sT rT]. +Arguments big_sub_widen [S idx op T sT rT]. (* -------------------------------------------------------------------- *) Section Product. diff --git a/src/xfinmap.v b/src/xfinmap.v index 16fe234..f6cde8e 100644 --- a/src/xfinmap.v +++ b/src/xfinmap.v @@ -71,7 +71,7 @@ by rewrite /index_enum -enumT mem_enum. Qed. End BigFSetIncl. -Implicit Arguments big_fset_incl [R idx op T A B]. +Arguments big_fset_incl [R idx op T A B]. (* -------------------------------------------------------------------- *) Module BigEnoughFSet.