Skip to content

Releases: imdea-software/fcsl-pcm

2.0.0

18 Sep 14:07
27560ef
Compare
Choose a tag to compare
  • A new major release based on mathcomp2.
  • Dropped coq8.15-8.17, support 8.19-8.20.
  • Complete revision of pcm, morphism, unionmap, and natmap hierarchies, based on Hierarchy Builder.
  • Expanded prelude, pred, seqext, slice, uconsec and useqord infrastructure.
  • Removed lift.

1.8.0

10 May 12:39
b2aa833
Compare
Choose a tag to compare
  • allow Coq 8.17, drop 8.14
  • allow Mathcomp 1.16, drop 1.13-14
  • add mathcomp-algebra dependency
  • add Prop-level theory for All and Has
  • rename AllPn->allPnIn, HasPn->hasPnIn
  • add trans_eq, if_triv, theory for foldl/r and onth in prelude, rename prefixP -> prefixE
  • expand seq theory in seqext, including "big cat" lemmas
  • refactor slice theory, split interval theory on unique sequences into useqord, uslice and uconsec

1.7.0

11 Nov 10:55
Compare
Choose a tag to compare
  • remove Program switches in options
  • switch namespace to pcm to disambiguate with FCSL proper
  • split out theory of filter/last/index and binary relations to seqext
  • add a theory of finding the last element by predicate
  • generalize intervals to arbitrary eqType
  • generalize sepit_perm and sepitF lemmas to Prop-level predicates
  • add umpreim_cond, umpreimPt, rangeF & umfilt_predC to unionmap

1.6.0

20 Sep 12:01
Compare
Choose a tag to compare
  • allow Coq 8.16
  • added a theory of non-symmetric separating relations
  • refactored the theory of sub-PCMs and local relations
  • added a theory of map prefixes for unionmaps
  • added boolean reflection and rcons/last lemmas to prelude, \In lemmas to pred
  • refactored automated lemma infrastructure
  • extracted sequence intervals into a separate sub-theory
  • added several natmap theories required by current FCSL examples (will be deprecated and removed in future releases): continuous & complete maps, leq surgery, exec & growth

1.5.1

29 Apr 11:18
Compare
Choose a tag to compare

Updated minimal required version of Coq to 8.14

1.5.0

29 Apr 11:17
ed74aa5
Compare
Choose a tag to compare
  • added automation for general PCMs (currently contains a single pullX automation)
  • factored out common automation infrastructure for PCMs and maps
  • added finite PCM products
  • added a PCM instance for option
  • major refactoring of the natmap theory
  • additions to prelude and the unionmap theory, speed up andP reflections

1.4.0

17 Nov 22:46
Compare
Choose a tag to compare

Update minimal required versions of the dependencies: Coq 8.13 and Mathcomp 1.12

  • added behd (remove the head/minimal key+value) function for finmap
  • added a class for omap-like functions on unionmaps
  • expanded theory for working with natmaps as histories
  • code updated according to the new requirements of dependencies: #[export] attributes, lemma renamings etc
  • removed problematic setoid for funext
  • removed deprecated subPCM construction

1.3.0

15 Oct 16:22
1d5b782
Compare
Choose a tag to compare

Minimum required versions of the dependencies: Coq 8.11 and Mathcomp 1.10

  • Refactor unionmap class
  • Add PCM morphisms and separation relations
  • Various additions and fixes

1.1.1

06 Jan 20:03
Compare
Choose a tag to compare
  • Add support for Mathcomp 1.10 and drop support for the previous version
  • Extend the range of supported Coq versions: 8.7 .. 8.11

1.2.0

06 Jan 20:19
Compare
Choose a tag to compare
  • Upgrade minimum required versions of the dependencies to Coq 8.10 and Mathcomp 1.10
  • Simplify some proofs
  • Various maintenance fixes: warnings, opam file tweaks