]> matita.cs.unibo.it Git - helm.git/log
helm.git
8 years ago- matex: support for alpha-conversion completed
Ferruccio Guidi [Sat, 30 Apr 2016 21:33:47 +0000 (21:33 +0000)]
- matex: support for alpha-conversion completed
- matex.sty: hyperlinks without labels
- registry: support or triples

8 years agoexportation of lambdadelta 1 with flavoured let recs
Ferruccio Guidi [Wed, 27 Apr 2016 16:25:05 +0000 (16:25 +0000)]
exportation of lambdadelta 1 with flavoured let recs

8 years ago- partial commit of rt_transition ...
Ferruccio Guidi [Fri, 22 Apr 2016 14:23:31 +0000 (14:23 +0000)]
- partial commit of rt_transition  ...
- renaming in equivalence, dynamic, examples

8 years agomilestone in basic_2 ...
Ferruccio Guidi [Mon, 18 Apr 2016 18:36:29 +0000 (18:36 +0000)]
milestone in basic_2 ...

8 years agoground_2: generic rt-transition counter
Ferruccio Guidi [Mon, 18 Apr 2016 18:30:57 +0000 (18:30 +0000)]
ground_2: generic rt-transition counter

8 years agoAs required by M. Maietti,
Ferruccio Guidi [Mon, 18 Apr 2016 15:29:33 +0000 (15:29 +0000)]
As required by M. Maietti,
cyclic sort hierarchies are now allowed through the "cyclic" keyword
so we can write:
universe cyclic constraint Type[U] < Type[U].
definition inconsistent: Type[U] ≝ Type[U].
matitaclean all is required after this commit

8 years agorefactoring to park the notions:
Ferruccio Guidi [Sat, 16 Apr 2016 22:01:54 +0000 (22:01 +0000)]
refactoring to park the notions:
lstas, unfold, crr, cir, cnr, crx, cix, cnx

8 years agouniversary milestone in basic_2
Ferruccio Guidi [Sat, 16 Apr 2016 12:53:51 +0000 (12:53 +0000)]
universary milestone in basic_2

8 years ago- former llpx_sn an lleq reactivated as lfxs and lfeq
Ferruccio Guidi [Sat, 16 Apr 2016 12:43:32 +0000 (12:43 +0000)]
- former llpx_sn an lleq reactivated as lfxs and lfeq

8 years ago- first working commit of the static component ..
Ferruccio Guidi [Tue, 12 Apr 2016 14:27:22 +0000 (14:27 +0000)]
- first working commit of the static component ..
- updates on some web pages

8 years ago- advances on drops
Ferruccio Guidi [Mon, 11 Apr 2016 17:15:40 +0000 (17:15 +0000)]
- advances on drops
- partial commit of the "static" component

8 years agorenaming ...
Ferruccio Guidi [Fri, 8 Apr 2016 21:34:02 +0000 (21:34 +0000)]
renaming ...

8 years agominor additions :)
Ferruccio Guidi [Fri, 8 Apr 2016 21:30:19 +0000 (21:30 +0000)]
minor additions :)

8 years agoupdate in ground_2 and basic_2
Ferruccio Guidi [Fri, 8 Apr 2016 20:52:38 +0000 (20:52 +0000)]
update in ground_2 and basic_2

8 years ago- commit of the "s_computation" component ...
Ferruccio Guidi [Fri, 8 Apr 2016 20:49:11 +0000 (20:49 +0000)]
- commit of the "s_computation" component ...
- additions in ground_2/relocation
- milestonee added in basic_2
- minor corrections

8 years agothe newly generated web pages ...
Ferruccio Guidi [Thu, 7 Apr 2016 13:50:13 +0000 (13:50 +0000)]
the newly generated web pages ...

8 years ago- advances in the site generation architecture
Ferruccio Guidi [Thu, 7 Apr 2016 13:34:39 +0000 (13:34 +0000)]
- advances in the site generation architecture
- more on OSN and on the disclaimer

8 years agoone file was missing
Ferruccio Guidi [Mon, 4 Apr 2016 22:17:16 +0000 (22:17 +0000)]
one file was missing

8 years agoEBNF definition of OSN begins ...
Ferruccio Guidi [Mon, 4 Apr 2016 22:16:36 +0000 (22:16 +0000)]
EBNF definition of OSN begins ...

8 years ago- initial description of OSN
Ferruccio Guidi [Sun, 3 Apr 2016 20:52:04 +0000 (20:52 +0000)]
- initial description of OSN
- ld_web: minor updates

8 years agoimages for Open Symbolic Notation (OSN)
Ferruccio Guidi [Sun, 3 Apr 2016 13:10:21 +0000 (13:10 +0000)]
images for Open Symbolic Notation (OSN)

8 years agoupdate in ground_2 and basic_2 ...
Ferruccio Guidi [Fri, 1 Apr 2016 21:31:50 +0000 (21:31 +0000)]
update in ground_2 and basic_2 ...

8 years ago- new component "s_transition" for the restored fqu and fquq
Ferruccio Guidi [Fri, 1 Apr 2016 21:26:20 +0000 (21:26 +0000)]
- new component "s_transition" for the restored fqu and fquq
- minor additions
- notation update
- partial commit in the "static" component to park da and lsubd

8 years ago- uniform relocations
Ferruccio Guidi [Thu, 31 Mar 2016 14:44:31 +0000 (14:44 +0000)]
- uniform relocations
- more results on at and after

8 years agominor correction on "source" production
Ferruccio Guidi [Mon, 28 Mar 2016 16:27:25 +0000 (16:27 +0000)]
minor correction on "source" production

8 years agominor additions ...
Ferruccio Guidi [Mon, 28 Mar 2016 16:04:59 +0000 (16:04 +0000)]
minor additions ...

8 years agoupdate in basic_2 and apps_2 ...
Ferruccio Guidi [Sun, 27 Mar 2016 16:43:13 +0000 (16:43 +0000)]
update in basic_2 and apps_2 ...

8 years ago- minor corrections
Ferruccio Guidi [Sun, 27 Mar 2016 16:39:33 +0000 (16:39 +0000)]
- minor corrections
- web pages for nasoc_2 and apps_2 are up again

8 years agoanother file was missing :(
Ferruccio Guidi [Fri, 25 Mar 2016 20:06:48 +0000 (20:06 +0000)]
another file was missing :(

8 years ago- probe: now includes source character count (was: mac)
Ferruccio Guidi [Fri, 25 Mar 2016 18:48:24 +0000 (18:48 +0000)]
- probe: now includes source character count (was: mac)
- lambdadelta: summaries are generated using the updated probe

8 years agosupport for printing the number of objects grouped by flavour
Ferruccio Guidi [Thu, 24 Mar 2016 12:23:19 +0000 (12:23 +0000)]
support for printing the number of objects grouped by flavour

8 years agomore files to commit .... :(
Ferruccio Guidi [Wed, 23 Mar 2016 19:13:00 +0000 (19:13 +0000)]
more files to commit .... :(

8 years ago- ng_kernel: we print the offending term when guarded_by_constructors fails
Ferruccio Guidi [Wed, 23 Mar 2016 19:10:29 +0000 (19:10 +0000)]
- ng_kernel: we print the offending term when guarded_by_constructors fails
- probe: we print the roots when more than one root is found
- lambdadelta: first working commit for the "relocation" component

8 years agoupdate in ground_2
Ferruccio Guidi [Mon, 21 Mar 2016 19:39:42 +0000 (19:39 +0000)]
update in ground_2

8 years agortmaps with finite colength
Ferruccio Guidi [Mon, 21 Mar 2016 19:36:29 +0000 (19:36 +0000)]
rtmaps with finite colength

8 years agoadvances in the theory of drops, lexs, and frees ...
Ferruccio Guidi [Fri, 18 Mar 2016 14:25:19 +0000 (14:25 +0000)]
advances in the theory of drops, lexs, and frees ...

8 years ago- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
Ferruccio Guidi [Sun, 13 Mar 2016 17:30:14 +0000 (17:30 +0000)]
- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
- source specifier on inductive/coinductive types (implies matitaclan all)
- minor additions

8 years ago- ground_2: some additions
Ferruccio Guidi [Thu, 10 Mar 2016 21:16:20 +0000 (21:16 +0000)]
- ground_2: some additions
- basic_2/grammar: added missing files

8 years agopartial commit in the relocation component to move some files ...
Ferruccio Guidi [Thu, 10 Mar 2016 21:12:43 +0000 (21:12 +0000)]
partial commit in the relocation component to move some files ...

8 years agomore results on after ...
Ferruccio Guidi [Mon, 7 Mar 2016 17:04:28 +0000 (17:04 +0000)]
more results on after ...

8 years agosmall improvements and corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:52:33 +0000 (19:52 +0000)]
small improvements and corrections ...

8 years agosome corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:51:20 +0000 (19:51 +0000)]
some corrections ...

8 years agomailstone in ground_2 ...
Ferruccio Guidi [Fri, 4 Mar 2016 15:18:05 +0000 (15:18 +0000)]
mailstone in ground_2 ...

8 years agocommitcompleted: some files were missing :(
Ferruccio Guidi [Fri, 4 Mar 2016 15:14:13 +0000 (15:14 +0000)]
commitcompleted: some files were missing :(

8 years agortmap (platform-indepent multple relocation): application and composition
Ferruccio Guidi [Fri, 4 Mar 2016 13:39:02 +0000 (13:39 +0000)]
rtmap (platform-indepent multple relocation): application and composition

8 years ago- second precommit for rtmap
Ferruccio Guidi [Wed, 2 Mar 2016 21:32:00 +0000 (21:32 +0000)]
- second precommit for rtmap
- we park relocation by streams of booleans

8 years agoprecommit for rtmap ...
Ferruccio Guidi [Tue, 23 Feb 2016 15:36:51 +0000 (15:36 +0000)]
precommit for rtmap ...

8 years agoMaTeX
Ferruccio Guidi [Sun, 21 Feb 2016 15:30:59 +0000 (15:30 +0000)]
MaTeX
- bug fixed in rendering of application: the head was not rendered sometimes
- we can generate the list of the produced TeX files
- TeX item for comments was missing
test
- bug fixed in matex.sty: pages were not ejected properly causig memory overflow
- now includes the whole \lambda\delta version 1 (737 pages for now)
- object numbering is now supported

8 years agonow every object is output in a LaTeX environment, not just proofs
Ferruccio Guidi [Mon, 15 Feb 2016 21:29:10 +0000 (21:29 +0000)]
now every object is output in a LaTeX environment, not just proofs

8 years agofirst commit for lreq ...
Ferruccio Guidi [Wed, 10 Feb 2016 19:02:11 +0000 (19:02 +0000)]
first commit for lreq ...

8 years ago- ground_2: update ...
Ferruccio Guidi [Wed, 10 Feb 2016 12:03:01 +0000 (12:03 +0000)]
- ground_2: update ...
- basic_2: first commit for lexs ...

8 years agopre commit for lexs ...
Ferruccio Guidi [Wed, 10 Feb 2016 11:20:14 +0000 (11:20 +0000)]
pre commit for lexs ...

8 years agogeneral slicing reactivated ...
Ferruccio Guidi [Tue, 9 Feb 2016 19:05:48 +0000 (19:05 +0000)]
general slicing reactivated ...

8 years agoupdate in ground_2
Ferruccio Guidi [Sun, 7 Feb 2016 17:55:13 +0000 (17:55 +0000)]
update in ground_2

8 years ago- ground_2: support for relocation updated
Ferruccio Guidi [Sun, 7 Feb 2016 17:45:09 +0000 (17:45 +0000)]
- ground_2: support for relocation updated
- basic_2: theory of relocation updated
- MaTeX: (co)inductive types are now processed

8 years ago- ground_2: relocation with nstream is now based on two basic functions (push and...
Ferruccio Guidi [Thu, 4 Feb 2016 15:35:23 +0000 (15:35 +0000)]
- ground_2: relocation with nstream is now based on two basic functions (push and next)
- matex: scope management completed! stylesheet improved (also with colors)

8 years ago- scope management completed
Ferruccio Guidi [Tue, 2 Feb 2016 16:52:55 +0000 (16:52 +0000)]
- scope management completed
- improved style sheet and test document

8 years ago- scope management begins...
Ferruccio Guidi [Tue, 2 Feb 2016 00:00:19 +0000 (00:00 +0000)]
- scope management begins...
- improved style sheet

8 years agoimproved style sheet
Ferruccio Guidi [Mon, 1 Feb 2016 00:20:16 +0000 (00:20 +0000)]
improved style sheet

8 years agorenaming ...
Ferruccio Guidi [Sun, 31 Jan 2016 14:37:43 +0000 (14:37 +0000)]
renaming ...

8 years agosome renaming ...
Ferruccio Guidi [Sat, 30 Jan 2016 14:10:38 +0000 (14:10 +0000)]
some renaming ...

8 years agolift functions and identity map
Ferruccio Guidi [Fri, 29 Jan 2016 14:48:27 +0000 (14:48 +0000)]
lift functions and identity map

8 years agolexicon commands must tbe parsed before grafite commands rather than
Ferruccio Guidi [Tue, 26 Jan 2016 16:09:51 +0000 (16:09 +0000)]
lexicon commands must tbe parsed before grafite commands rather than
after (why?)

8 years agodocumentation update
Ferruccio Guidi [Sat, 23 Jan 2016 08:51:34 +0000 (08:51 +0000)]
documentation update

8 years agonstream: composition completed :)
Ferruccio Guidi [Wed, 20 Jan 2016 21:37:35 +0000 (21:37 +0000)]
nstream: composition completed :)

8 years agoground_2: web page update
Ferruccio Guidi [Thu, 14 Jan 2016 22:19:57 +0000 (22:19 +0000)]
ground_2: web page update

8 years agomissing notation file
Ferruccio Guidi [Wed, 13 Jan 2016 20:35:12 +0000 (20:35 +0000)]
missing notation file

8 years ago- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i...
Ferruccio Guidi [Wed, 13 Jan 2016 20:33:18 +0000 (20:33 +0000)]
- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i < 1)
- ground_1: relocation with streams of natural numbers begins

8 years ago- plain anticipation for CIC proofs terms
Ferruccio Guidi [Mon, 11 Jan 2016 16:46:16 +0000 (16:46 +0000)]
- plain anticipation for CIC proofs terms
- support for (co)fixpoint objects
- Makefile for testing
- minor updates

8 years ago- Const is now processed properly
Ferruccio Guidi [Mon, 4 Jan 2016 12:33:52 +0000 (12:33 +0000)]
- Const is now processed properly

8 years agomore minor bugs fixed in the web site
Ferruccio Guidi [Wed, 30 Dec 2015 14:35:04 +0000 (14:35 +0000)]
more minor bugs fixed in the web site

8 years agominor bugs fixed in the web site, and minor updates
Ferruccio Guidi [Wed, 30 Dec 2015 14:06:17 +0000 (14:06 +0000)]
minor bugs fixed in the web site, and minor updates

8 years agosite update for helena 0.8.3
Ferruccio Guidi [Wed, 30 Dec 2015 12:02:25 +0000 (12:02 +0000)]
site update for helena 0.8.3

8 years ago- final commit for helena 0.8.3
Ferruccio Guidi [Tue, 29 Dec 2015 15:11:23 +0000 (15:11 +0000)]
- final commit for helena 0.8.3
  minir bugs fixed

8 years agominor bug fixes ...
Ferruccio Guidi [Sat, 26 Dec 2015 19:06:41 +0000 (19:06 +0000)]
minor bug fixes ...

8 years agobug fixes ...
Ferruccio Guidi [Sat, 26 Dec 2015 18:57:21 +0000 (18:57 +0000)]
bug fixes ...

8 years agobyproducts of compilation ignored for svn
Ferruccio Guidi [Mon, 21 Dec 2015 15:18:16 +0000 (15:18 +0000)]
byproducts of compilation ignored for svn

8 years ago- First commit of MaTeX:
Ferruccio Guidi [Mon, 21 Dec 2015 15:13:18 +0000 (15:13 +0000)]
- First commit of MaTeX:
  an utility for typesetting the terms produced by matita il LaTeX

- The AST nodes of terms are output as LaTeX macros

- The user configures the desired rendering of terms by
  defining these macros in a LaTeX stylesheet

- Each term inside objects is output in a separate file
  for easy inclusion in the main document

- This softare originates from "coqpp", our appication with which
  Coq terms were typeset in UBLCS 2006-01

as of now,
only Constant objects are accepted and
Const is not processed properly

8 years agoweb site minor update
Ferruccio Guidi [Thu, 10 Dec 2015 17:26:32 +0000 (17:26 +0000)]
web site minor update

8 years agoweb site update
Ferruccio Guidi [Thu, 10 Dec 2015 15:31:42 +0000 (15:31 +0000)]
web site update

9 years agoupdate in ground_2
Ferruccio Guidi [Fri, 30 Oct 2015 11:48:09 +0000 (11:48 +0000)]
update in ground_2

9 years ago- matita: computed auto traces now include the "width" parameter
Ferruccio Guidi [Thu, 29 Oct 2015 22:46:45 +0000 (22:46 +0000)]
- matita: computed auto traces now include the "width" parameter
          more characters for use with lambdadelta
- ground_2: advances in relocation by trace

9 years agotheory of relocation updated .....
Ferruccio Guidi [Sun, 25 Oct 2015 18:58:13 +0000 (18:58 +0000)]
theory of relocation updated .....

9 years agotheory of generic slicing almost completed ....
Ferruccio Guidi [Sun, 25 Oct 2015 18:56:33 +0000 (18:56 +0000)]
theory of generic slicing almost completed ....

9 years agoparked material ...
Ferruccio Guidi [Wed, 21 Oct 2015 17:05:02 +0000 (17:05 +0000)]
parked material ...

9 years agonew results on multiple relocation
Ferruccio Guidi [Wed, 21 Oct 2015 17:00:58 +0000 (17:00 +0000)]
new results on multiple relocation

9 years agotheory of multiple relocation completed
Ferruccio Guidi [Wed, 21 Oct 2015 16:59:38 +0000 (16:59 +0000)]
theory of multiple relocation completed

9 years agominor update
Ferruccio Guidi [Wed, 21 Oct 2015 16:50:43 +0000 (16:50 +0000)]
minor update

9 years agostats updated for ground_2
Ferruccio Guidi [Wed, 14 Oct 2015 19:47:34 +0000 (19:47 +0000)]
stats updated for ground_2

9 years agocommit in ground_2
Ferruccio Guidi [Wed, 14 Oct 2015 19:44:30 +0000 (19:44 +0000)]
commit in ground_2

9 years agocolength and identity relocation
Ferruccio Guidi [Wed, 14 Oct 2015 19:42:43 +0000 (19:42 +0000)]
colength and identity relocation

9 years agomilestone in ground_2
Ferruccio Guidi [Sun, 11 Oct 2015 15:45:32 +0000 (15:45 +0000)]
milestone in ground_2

9 years agoground_2: added missing file
Ferruccio Guidi [Sun, 11 Oct 2015 15:02:58 +0000 (15:02 +0000)]
ground_2: added missing file
basic_2: commit of grammar completed

9 years agoground_2 milestone: multiple relocation with lists of booleans
Ferruccio Guidi [Sun, 11 Oct 2015 14:39:30 +0000 (14:39 +0000)]
ground_2 milestone: multiple relocation with lists of booleans
basic_2: simplified formalization starts: partial commit of the grammar component

9 years agofirst constructions with classes
Ferruccio Guidi [Thu, 24 Sep 2015 14:03:26 +0000 (14:03 +0000)]
first constructions with classes

9 years agooptional parameters added to the syntax of definitions,
Ferruccio Guidi [Wed, 23 Sep 2015 11:32:08 +0000 (11:32 +0000)]
optional parameters added to the syntax of definitions,
like the one for Record and Inductive.

9 years agolimits: we set up a different foundation
Ferruccio Guidi [Sun, 20 Sep 2015 18:49:03 +0000 (18:49 +0000)]
limits: we set up a different foundation
lambdadelta: Makefile updated for new version of probe

9 years agoold files (re)moved
Ferruccio Guidi [Sun, 20 Sep 2015 17:52:45 +0000 (17:52 +0000)]
old files (re)moved

9 years agominor site update
Ferruccio Guidi [Sat, 12 Sep 2015 21:00:04 +0000 (21:00 +0000)]
minor site update

9 years agorefactoring meta files for procedural reconstruction of \lambda\delta version 1
Ferruccio Guidi [Tue, 8 Sep 2015 13:40:09 +0000 (13:40 +0000)]
refactoring meta files for procedural reconstruction of \lambda\delta version 1