Ssreflect Users Discussion List

[Erik Martin-Dorel <>]

Hello,

I have four minor remarks related to the release candidates:

1) With ssreflect-1.5rc1.tar.gz: $(make clean) raises an error
> "rm: cannot remove `bin': Is a directory"
I thus needed to replace
================8<
        rm -f $(COQMAKEFILE) bin
================8<================
with
================8<
        rm -f $(COQMAKEFILE)
        rm -f -r bin
================8<================
in ssreflect-1.5/Makefile


2) I also tested the static compilation, and once the plug-in has been
compiled with Coq 8.4pl2, I get the error
> bin/ssrcoq -q  -I src -R theories Ssreflect   -compile theories/ssrmatching
> Error: cannot guess a path for Coq libraries; please use -coqlib option
So I needed to replace
================8<
#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
================8<================
with
================8<
-custom "$(SSRCOQ) -coqlib `$(COQBIN)coqtop -where` $(COQFLAGS) -compile 
$*" "%.v $(SSRCOQ)" "%.vo"
================8<================
in ssreflect-1.5/Make


3) As regards "mathcomp-1.5rc1.tar.gz", would it be worth it to use
the same wrapper as ssreflect-1.5/Makefile for adding a trailing slash
to COQBIN ? That is, putting
================8<
ifneq "$(COQBIN)" ""
        COQBIN := $(COQBIN)/
endif
================8<================
at the beginning of mathcomp-1.5/Makefile ?


4) Finally I would like to propose a workaround related to the
pretty-printing of some MathComp notations: if we issue for example
================8<
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice 
fintype.
Require Import bigop ssralg binomial.
Search _ in ssralg.
================8<================
some theorem types such as the following cannot be parsed back due to
the comment characters "(*" :
================8<
GRing.signrMK  forall (R : ringType) (n : nat), involutive (*%R ((-1) ^+ n))
================8<================
So I added a space in each "*%R"-like notation as described in the
attached patch, and it seems to work smoothly: we get
================8<
GRing.signrMK  forall (R : ringType) (n : nat), involutive ( *%R ((-1) 
^+ n))
================8<================
What is your opinon on this change?


Kind regards,

Erik

On 08/05/2013 12:50 PM, Enrico Tassi wrote:
> Hello, I'm preparing a release for ssreflect and the mathematical
> components library.  From this release the proof language and the
> library are distributed as separate packages.
>
> The proof language package (ssreflect) contains the coq plugin plus
> the .v files up to finType, while the rest of the .v files are
> distributed in the library package (mathcomp).
>
> Release candidate tarballs are available here:
>    http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5rc1.tar.gz
>    http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5rc1.tar.gz
>
> All packages are for Coq 8.4 and CamlP5.  The user manual is already up
> to date w.r.t. the few changes in the proof language:
>    http://hal.inria.fr/inria-00258384
>
> And now the request for comments.
>
> For the users:
> - Please test the archive(s) you are interested in
>
> For the mathcomp authors:
> - While I'm pretty sure the ssreflect archive is fine, I did put
>    in the mathcomp one only the files that were in the 1.4 release.
>    If some other file reached maturity, please tell me or (better)
>    edit dist-MathComp/Make
>
> Cheers

--
Érik Martin-Dorel
Post-doctorant, Équipe-projet Marelle
Inria Sophia Antipolis - Méditerranée
http://erik.martin-dorel.org/
diff -u -r a/mathcomp-1.5/theories/bigop.v b/mathcomp-1.5/theories/bigop.v
--- a/mathcomp-1.5/theories/bigop.v	2013-08-05 11:32:45.000000000 +0200
+++ b/mathcomp-1.5/theories/bigop.v	2013-08-05 19:11:29.522099686 +0200
@@ -614,7 +614,7 @@
 Notation "\sum_ ( i 'in' A ) F" :=
   (\big[+%N/0%N]_(i in A) F%N) : nat_scope.
 
-Local Notation "*%N" := muln (at level 0, only parsing).
+Local Notation "  *%N" := muln (at level 0, only parsing).
 Notation "\prod_ ( i <- r | P ) F" :=
   (\big[*%N/1%N]_(i <- r | P%B) F%N) : nat_scope.
 Notation "\prod_ ( i <- r ) F" :=
@@ -1078,7 +1078,7 @@
 
 Variable op : Monoid.law 1.
 
-Notation Local "*%M" := op (at level 0).
+Notation Local "  *%M" := op (at level 0).
 Notation Local "x * y" := (op x y).
 
 Lemma eq_big_idx_seq idx' I r (P : pred I) F :
@@ -1491,7 +1491,7 @@
 Notation Local "0" := zero.
 Notation Local "1" := one.
 Variable times : Monoid.mul_law 0.
-Notation Local "*%M" := times (at level 0).
+Notation Local "  *%M" := times (at level 0).
 Notation Local "x * y" := (times x y).
 Variable plus : Monoid.add_law 0 *%M.
 Notation Local "+%M" := plus (at level 0).
diff -u -r a/mathcomp-1.5/theories/ssralg.v b/mathcomp-1.5/theories/ssralg.v
--- a/mathcomp-1.5/theories/ssralg.v	2013-08-05 11:32:45.000000000 +0200
+++ b/mathcomp-1.5/theories/ssralg.v	2013-08-05 18:52:25.600317596 +0200
@@ -558,7 +558,8 @@
 
 Reserved Notation "+%R" (at level 0).
 Reserved Notation "-%R" (at level 0).
-Reserved Notation "*%R" (at level 0).
+Reserved Notation "  *%R" (at level 0).
+Reserved Notation "  *:%R" (at level 0).
 Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").
 Reserved Notation "k %:A" (at level 2, left associativity, format "k %:A").
 Reserved Notation "[ 'char' F ]" (at level 0, format "[ 'char'  F ]").
@@ -915,7 +916,7 @@
 Local Notation "1" := (one _) : ring_scope.
 Local Notation "- 1" := (- (1)) : ring_scope.
 Local Notation "n %:R" := (1 *+ n) : ring_scope.
-Local Notation "*%R" := (@mul _).
+Local Notation "  *%R" := (@mul _).
 Local Notation "x * y" := (mul x y) : ring_scope.
 Local Notation "x ^+ n" := (exp x n) : ring_scope.
 
@@ -1508,7 +1509,7 @@
 Definition scale (R : ringType) (V : lmodType R) :=
   Lmodule.scale (Lmodule.class V).
 
-Local Notation "*:%R" := (@scale _ _).
+Local Notation "  *:%R" := (@scale _ _).
 Local Notation "a *: v" := (scale a v) : ring_scope.
 
 Section LmoduleTheory.
@@ -1516,7 +1517,7 @@
 Variables (R : ringType) (V : lmodType R).
 Implicit Types (a b c : R) (u v : V).
 
-Local Notation "*:%R" := (@scale R V).
+Local Notation "  *:%R" := (@scale R V).
 
 Lemma scalerA a b v : a *: (b *: v) = a * b *: v.
 Proof. by case: V v => ? [] ? []. Qed.
@@ -5694,14 +5695,14 @@
 Notation "n %:R" := (natmul 1 n) : ring_scope.
 Notation "[ 'char' R ]" := (char (Phant R)) : ring_scope.
 Notation Frobenius_aut chRp := (Frobenius_aut chRp).
-Notation "*%R" := (@mul _).
+Notation "  *%R" := (@mul _).
 Notation "x * y" := (mul x y) : ring_scope.
 Notation "x ^+ n" := (exp x n) : ring_scope.
 Notation "x ^-1" := (inv x) : ring_scope.
 Notation "x ^- n" := (inv (x ^+ n)) : ring_scope.
 Notation "x / y" := (mul x y^-1) : ring_scope.
 
-Notation "*:%R" := (@scale _ _).
+Notation "  *:%R" := (@scale _ _).
 Notation "a *: m" := (scale a m) : ring_scope.
 Notation "k %:A" := (scale k 1) : ring_scope.
 Notation "\0" := (null_fun _) : ring_scope.
diff -u -r a/mathcomp-1.5/theories/ssrint.v b/mathcomp-1.5/theories/ssrint.v
--- a/mathcomp-1.5/theories/ssrint.v	2013-08-05 11:32:46.000000000 +0200
+++ b/mathcomp-1.5/theories/ssrint.v	2013-08-05 18:52:25.601317589 +0200
@@ -246,7 +246,7 @@
   end.
 
 Local Notation "1" := (1%N:int) : int_scope.
-Local Notation "*%Z" := (@mulz) : int_scope.
+Local Notation "  *%Z" := (@mulz) (at level 0) : int_scope.
 Local Notation "x * y" := (mulz x y) : int_scope.
 
 Lemma mul0z : left_zero 0 *%Z.
@@ -489,7 +489,7 @@
     | Negz n => (x *- (n.+1))%R
   end.
 
-Notation "*~%R" := (@intmul _) (at level 0) : ring_scope.
+Notation "  *~%R" := (@intmul _) (at level 0) : ring_scope.
 Notation "x *~ n" := (intmul x n)
   (at level 40, left associativity, format "x  *~  n") : ring_scope.
 Notation intr := ( *~%R 1).