coq-mathcomp/mathcomp/Make.test-suite, branch master Library of mathematical components formalized in Coq Turn class_of records into primitive records and get rid of the xclass idiom 2020-10-07T14:23:26+00:00 Kazuhiko Sakaguchi 2020-09-10T12:19:55+00:00 ad55cb4128382852370ea53d36f4d21a83274e8b 






test-suite works both in local and system wide mode
2020-09-14T11:58:24+00:00

Enrico Tassi

2020-09-14T11:58:24+00:00

755068fd34f0fa1e918123c4859aef2e89bedfca












Fix some Makefile issues and rename `hierarchy_test.v` to `test_hierarchy_all.v`
2020-06-27T04:10:12+00:00

Kazuhiko Sakaguchi

2020-06-15T17:11:03+00:00

36613c83d65aa821b01a9fac38c479af65ef3589












adding guard conditions check to the test_suite
2020-04-10T10:25:12+00:00

Cyril Cohen

2020-04-10T08:55:30+00:00

b4673a3f6d06a4ff38789fd82f33dd517186eb44












Rewriting with AC (not modulo AC), using a small scale command.
2020-04-06T10:40:23+00:00

Cyril Cohen

2018-03-21T08:01:11+00:00

a0d310fef7b4023793e74af103955e2dd8832faf

This replaces opA, opC, opAC, opCA, ... and any combinations of them

- Right now the rewrite relies on an rather efficient computation
  of perm_eq using a "spaghetti sort" in O(n log n)
- Wrongly formed AC statements send error messages showing the
  discrepancy between LHS and RHS patterns.

 Usage :
   rewrite [pattern](AC operator pattern-shape re-ordering)
   rewrite [pattern](ACl operator re-ordering)

 - pattern is optional, as usual,
 - operator must have a canonical Monoid.com_law structure
   (additions, multiplications, conjunction and disjunction do)
 - pattern-shape is expressed using the syntax
      p := n | p * p'
      where "*" is purely formal
        and n > 0 is number of left associated symbols
   examples of pattern shapes:
   + 4 represents (n * m * p * q)
   + (1*2) represents (n * (m * p))
 - re-ordering is expressed using the syntax
     s := n | s * s'
   where "*" is purely formal and n is the position in the LHS

 If the ACl variant is used, the pattern-shape defaults to the
 pattern fully associated to the left i.e. n i.e (x * y * ...)

 Examples of re-orderings:
 - ACl op ((0*1)*2) is the identity (and should fail to rewrite)
 - opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1)
 - opCA == AC op (2*1) (0*1*2)
 - rewrite opCA -opA == rewrite (ACl op (0*(2*1))
 - opACA == AC (2*2) ((0*2)*(1*3))





This replaces opA, opC, opAC, opCA, ... and any combinations of them

- Right now the rewrite relies on an rather efficient computation
  of perm_eq using a "spaghetti sort" in O(n log n)
- Wrongly formed AC statements send error messages showing the
  discrepancy between LHS and RHS patterns.

 Usage :
   rewrite [pattern](AC operator pattern-shape re-ordering)
   rewrite [pattern](ACl operator re-ordering)

 - pattern is optional, as usual,
 - operator must have a canonical Monoid.com_law structure
   (additions, multiplications, conjunction and disjunction do)
 - pattern-shape is expressed using the syntax
      p := n | p * p'
      where "*" is purely formal
        and n > 0 is number of left associated symbols
   examples of pattern shapes:
   + 4 represents (n * m * p * q)
   + (1*2) represents (n * (m * p))
 - re-ordering is expressed using the syntax
     s := n | s * s'
   where "*" is purely formal and n is the position in the LHS

 If the ACl variant is used, the pattern-shape defaults to the
 pattern fully associated to the left i.e. n i.e (x * y * ...)

 Examples of re-orderings:
 - ACl op ((0*1)*2) is the identity (and should fail to rewrite)
 - opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1)
 - opCA == AC op (2*1) (0*1*2)
 - rewrite opCA -opA == rewrite (ACl op (0*(2*1))
 - opACA == AC (2*2) ((0*2)*(1*3))







Fix and improve the test suite and Makefile
2019-10-02T09:23:14+00:00

Kazuhiko Sakaguchi

2019-09-26T07:48:48+00:00

a899bb7ef1d6a2c35b1b9a646dfeae332972f5f6

- improve an error message produced by the `check_join` tactic,
- fix the build of the test suite: `make test-suite`, and
- add a new rule `only` to build a subset of MathComp.





- improve an error message produced by the `check_join` tactic,
- fix the build of the test suite: `make test-suite`, and
- add a new rule `only` to build a subset of MathComp.