]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Mon, 28 Mar 2016 16:04:59 +0000 (16:04 +0000)]
minor additions ...
Ferruccio Guidi [Sun, 27 Mar 2016 16:43:13 +0000 (16:43 +0000)]
update in basic_2 and apps_2 ...
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
Ferruccio Guidi [Fri, 25 Mar 2016 20:06:48 +0000 (20:06 +0000)]
another file was missing :(
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
Ferruccio Guidi [Thu, 24 Mar 2016 12:23:19 +0000 (12:23 +0000)]
support for printing the number of objects grouped by flavour
Ferruccio Guidi [Wed, 23 Mar 2016 19:13:00 +0000 (19:13 +0000)]
more files to commit .... :(
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
Ferruccio Guidi [Mon, 21 Mar 2016 19:39:42 +0000 (19:39 +0000)]
update in ground_2
Ferruccio Guidi [Mon, 21 Mar 2016 19:36:29 +0000 (19:36 +0000)]
rtmaps with finite colength
Ferruccio Guidi [Fri, 18 Mar 2016 14:25:19 +0000 (14:25 +0000)]
advances in the theory of drops, lexs, and frees ...
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
Ferruccio Guidi [Thu, 10 Mar 2016 21:16:20 +0000 (21:16 +0000)]
- ground_2: some additions
- basic_2/grammar: added missing files
Ferruccio Guidi [Thu, 10 Mar 2016 21:12:43 +0000 (21:12 +0000)]
partial commit in the relocation component to move some files ...
Ferruccio Guidi [Mon, 7 Mar 2016 17:04:28 +0000 (17:04 +0000)]
more results on after ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:52:33 +0000 (19:52 +0000)]
small improvements and corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:51:20 +0000 (19:51 +0000)]
some corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 15:18:05 +0000 (15:18 +0000)]
mailstone in ground_2 ...
Ferruccio Guidi [Fri, 4 Mar 2016 15:14:13 +0000 (15:14 +0000)]
commitcompleted: some files were missing :(
Ferruccio Guidi [Fri, 4 Mar 2016 13:39:02 +0000 (13:39 +0000)]
rtmap (platform-indepent multple relocation): application and composition
Ferruccio Guidi [Wed, 2 Mar 2016 21:32:00 +0000 (21:32 +0000)]
- second precommit for rtmap
- we park relocation by streams of booleans
Ferruccio Guidi [Tue, 23 Feb 2016 15:36:51 +0000 (15:36 +0000)]
precommit for rtmap ...
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
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
Ferruccio Guidi [Wed, 10 Feb 2016 19:02:11 +0000 (19:02 +0000)]
first commit for lreq ...
Ferruccio Guidi [Wed, 10 Feb 2016 12:03:01 +0000 (12:03 +0000)]
- ground_2: update ...
- basic_2: first commit for lexs ...
Ferruccio Guidi [Wed, 10 Feb 2016 11:20:14 +0000 (11:20 +0000)]
pre commit for lexs ...
Ferruccio Guidi [Tue, 9 Feb 2016 19:05:48 +0000 (19:05 +0000)]
general slicing reactivated ...
Ferruccio Guidi [Sun, 7 Feb 2016 17:55:13 +0000 (17:55 +0000)]
update in ground_2
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
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)
Ferruccio Guidi [Tue, 2 Feb 2016 16:52:55 +0000 (16:52 +0000)]
- scope management completed
- improved style sheet and test document
Ferruccio Guidi [Tue, 2 Feb 2016 00:00:19 +0000 (00:00 +0000)]
- scope management begins...
- improved style sheet
Ferruccio Guidi [Mon, 1 Feb 2016 00:20:16 +0000 (00:20 +0000)]
improved style sheet
Ferruccio Guidi [Sun, 31 Jan 2016 14:37:43 +0000 (14:37 +0000)]
renaming ...
Ferruccio Guidi [Sat, 30 Jan 2016 14:10:38 +0000 (14:10 +0000)]
some renaming ...
Ferruccio Guidi [Fri, 29 Jan 2016 14:48:27 +0000 (14:48 +0000)]
lift functions and identity map
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?)
Ferruccio Guidi [Sat, 23 Jan 2016 08:51:34 +0000 (08:51 +0000)]
documentation update
Ferruccio Guidi [Wed, 20 Jan 2016 21:37:35 +0000 (21:37 +0000)]
nstream: composition completed :)
Ferruccio Guidi [Thu, 14 Jan 2016 22:19:57 +0000 (22:19 +0000)]
ground_2: web page update
Ferruccio Guidi [Wed, 13 Jan 2016 20:35:12 +0000 (20:35 +0000)]
missing notation file
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
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
Ferruccio Guidi [Mon, 4 Jan 2016 12:33:52 +0000 (12:33 +0000)]
- Const is now processed properly
Ferruccio Guidi [Wed, 30 Dec 2015 14:35:04 +0000 (14:35 +0000)]
more minor bugs fixed in the web site
Ferruccio Guidi [Wed, 30 Dec 2015 14:06:17 +0000 (14:06 +0000)]
minor bugs fixed in the web site, and minor updates
Ferruccio Guidi [Wed, 30 Dec 2015 12:02:25 +0000 (12:02 +0000)]
site update 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
Ferruccio Guidi [Sat, 26 Dec 2015 19:06:41 +0000 (19:06 +0000)]
minor bug fixes ...
Ferruccio Guidi [Sat, 26 Dec 2015 18:57:21 +0000 (18:57 +0000)]
bug fixes ...
Ferruccio Guidi [Mon, 21 Dec 2015 15:18:16 +0000 (15:18 +0000)]
byproducts of compilation ignored for svn
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
Ferruccio Guidi [Thu, 10 Dec 2015 17:26:32 +0000 (17:26 +0000)]
web site minor update
Ferruccio Guidi [Thu, 10 Dec 2015 15:31:42 +0000 (15:31 +0000)]
web site update
Ferruccio Guidi [Fri, 30 Oct 2015 11:48:09 +0000 (11:48 +0000)]
update in ground_2
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
Ferruccio Guidi [Sun, 25 Oct 2015 18:58:13 +0000 (18:58 +0000)]
theory of relocation updated .....
Ferruccio Guidi [Sun, 25 Oct 2015 18:56:33 +0000 (18:56 +0000)]
theory of generic slicing almost completed ....
Ferruccio Guidi [Wed, 21 Oct 2015 17:05:02 +0000 (17:05 +0000)]
parked material ...
Ferruccio Guidi [Wed, 21 Oct 2015 17:00:58 +0000 (17:00 +0000)]
new results on multiple relocation
Ferruccio Guidi [Wed, 21 Oct 2015 16:59:38 +0000 (16:59 +0000)]
theory of multiple relocation completed
Ferruccio Guidi [Wed, 21 Oct 2015 16:50:43 +0000 (16:50 +0000)]
minor update
Ferruccio Guidi [Wed, 14 Oct 2015 19:47:34 +0000 (19:47 +0000)]
stats updated for ground_2
Ferruccio Guidi [Wed, 14 Oct 2015 19:44:30 +0000 (19:44 +0000)]
commit in ground_2
Ferruccio Guidi [Wed, 14 Oct 2015 19:42:43 +0000 (19:42 +0000)]
colength and identity relocation
Ferruccio Guidi [Sun, 11 Oct 2015 15:45:32 +0000 (15:45 +0000)]
milestone in ground_2
Ferruccio Guidi [Sun, 11 Oct 2015 15:02:58 +0000 (15:02 +0000)]
ground_2: added missing file
basic_2: commit of grammar completed
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
Ferruccio Guidi [Thu, 24 Sep 2015 14:03:26 +0000 (14:03 +0000)]
first constructions with classes
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.
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
Ferruccio Guidi [Sun, 20 Sep 2015 17:52:45 +0000 (17:52 +0000)]
old files (re)moved
Ferruccio Guidi [Sat, 12 Sep 2015 21:00:04 +0000 (21:00 +0000)]
minor site update
Ferruccio Guidi [Tue, 8 Sep 2015 13:40:09 +0000 (13:40 +0000)]
refactoring meta files for procedural reconstruction of \lambda\delta version 1
Ferruccio Guidi [Mon, 7 Sep 2015 15:03:43 +0000 (15:03 +0000)]
- simplified Makefile.defs using the ?= assignment
- now the variable OCAMLPATH is available and is correctly set
Ferruccio Guidi [Sun, 6 Sep 2015 19:43:23 +0000 (19:43 +0000)]
scripts for lambdadelta_1 updated with minor corrections
Ferruccio Guidi [Sun, 6 Sep 2015 19:22:38 +0000 (19:22 +0000)]
- the `Implied attribute is now printed
[also the `Generated attribute is printed. is this ok?]
Ferruccio Guidi [Sun, 6 Sep 2015 17:42:29 +0000 (17:42 +0000)]
flavour and source information exported for the objects of lambdadelta version 1
Ferruccio Guidi [Sat, 5 Sep 2015 15:36:06 +0000 (15:36 +0000)]
last comment was incomplete by mistake.
- Rationale
The `Implied attribute will mark the eliminators generated by Coq
7.3.1 added to the contrib of lambdadelta version 1.
[the latest version of matita generates different eliminators to
Prop (with dependences) so we cannot reuse them]
However, these eliminators, even if provided, must not be taken into
account when calculating the intrinsinc complexity of the contribution
on the matita side (by the "probe" tool), because they are not taken into
account on the Coq side, being `Generated by Coq.
Note that the intrinsinc complexity we are interested in is the one
accounting just for the user-defined objects in both contributions.
- probe: updated to handle the `Implied attribute
- .depend: updated
Ferruccio Guidi [Sat, 5 Sep 2015 15:14:26 +0000 (15:14 +0000)]
- New attribute `Implied put beside `Generated and `Provided.
It denotes an object provided not as defined by the user, but as generated by another ITP
New optional keyword "implied" recognized in front of:
theorem, definition, ..., let rec, let corec
specifies to construct an object with this new attribute.
[still not admitted in front of inductive, coinductive, record]
Ferruccio Guidi [Fri, 4 Sep 2015 17:13:24 +0000 (17:13 +0000)]
typo corrected in bibliography
Ferruccio Guidi [Wed, 2 Sep 2015 16:05:37 +0000 (16:05 +0000)]
last commit completed :)
Ferruccio Guidi [Wed, 2 Sep 2015 16:01:28 +0000 (16:01 +0000)]
updated bibliography
Ferruccio Guidi [Fri, 7 Aug 2015 12:28:18 +0000 (12:28 +0000)]
new version of J3a submitted to JFR
Ferruccio Guidi [Tue, 14 Jul 2015 17:38:33 +0000 (17:38 +0000)]
- subtraction (and related notions) removed
- more lemmas
Ferruccio Guidi [Tue, 7 Jul 2015 19:57:05 +0000 (19:57 +0000)]
compile-time feature PROFV to profile validation without sort inclusion
Ferruccio Guidi [Tue, 7 Jul 2015 16:10:54 +0000 (16:10 +0000)]
grundlagen for coq with timing information
Ferruccio Guidi [Tue, 7 Jul 2015 15:44:51 +0000 (15:44 +0000)]
= test2 for byte and opt
- version string management updated
Ferruccio Guidi [Mon, 6 Jul 2015 21:52:17 +0000 (21:52 +0000)]
- multi-file exportation for teyjus
- more profiling for helena and coq
Ferruccio Guidi [Sun, 5 Jul 2015 14:36:36 +0000 (14:36 +0000)]
more flexibility in the exported data for Teyjus
Ferruccio Guidi [Sat, 4 Jul 2015 13:37:33 +0000 (13:37 +0000)]
- conditional compilation continues ...
- current run times for helena and managers in profile.txt
Ferruccio Guidi [Thu, 2 Jul 2015 21:27:48 +0000 (21:27 +0000)]
initial support for bytecode compilation
Ferruccio Guidi [Wed, 1 Jul 2015 19:00:12 +0000 (19:00 +0000)]
- simpler attribute system
- some renaming
Ferruccio Guidi [Mon, 29 Jun 2015 20:29:12 +0000 (20:29 +0000)]
we are optimizing the code by conditional compilation.
three tags introduced so far: EXPAND, PREPROCESS, MANAGER
Ferruccio Guidi [Sun, 28 Jun 2015 18:47:24 +0000 (18:47 +0000)]
new semantics of the -g option completed
Ferruccio Guidi [Sat, 27 Jun 2015 18:35:52 +0000 (18:35 +0000)]
- bug fix in the static analyzer allows better Pi/forall separation (exportation to grafite)
- new option -y allows to use infinity-abstraction in contexts
- ages removed from global references (the RTM computes them)
- new semantics of the -g option (w.i.p.) for a comparison with Coq
Ferruccio Guidi [Thu, 25 Jun 2015 19:00:51 +0000 (19:00 +0000)]
advances on exportation to prolog
Ferruccio Guidi [Mon, 22 Jun 2015 17:53:25 +0000 (17:53 +0000)]
command line options rearranged
Ferruccio Guidi [Fri, 19 Jun 2015 16:58:43 +0000 (16:58 +0000)]
new options activated
- tracing can be restricted to specific constants with -b and -e
- restricted applications are now used by default for Automath inputs
use -n to activate extended applications
(this may lead to longer computations)