]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agoFixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
Wilmer Ricciotti [Wed, 17 Apr 2013 10:50:45 +0000 (10:50 +0000)]
Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
lemma with unskipped goals closed by side-effect.

11 years agomilestone update in basic_2!
Ferruccio Guidi [Tue, 16 Apr 2013 19:52:17 +0000 (19:52 +0000)]
milestone update in basic_2!

11 years ago- we commit just the components before "reducibility"
Ferruccio Guidi [Tue, 16 Apr 2013 19:45:41 +0000 (19:45 +0000)]
- we commit just the components before "reducibility"
- reaxiomatized substitution and reduction now commute with respect to
subclosure
- delift and thin removed for now

11 years agouncommited file found :)
Ferruccio Guidi [Mon, 15 Apr 2013 17:55:59 +0000 (17:55 +0000)]
uncommited file found :)

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:44:22 +0000 (11:44 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:43:43 +0000 (11:43 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 11:32:54 +0000 (11:32 +0000)]
commit by user andrea

11 years agocommit by user andrea
matitaweb [Wed, 10 Apr 2013 10:01:59 +0000 (10:01 +0000)]
commit by user andrea

11 years agoFixes a bug that caused an assertion failure when no notation was defined.
Wilmer Ricciotti [Tue, 9 Apr 2013 13:41:15 +0000 (13:41 +0000)]
Fixes a bug that caused an assertion failure when no notation was defined.

11 years agoPatch by Paolo Tranquilli. It fixes the following problem: when a new
Claudio Sacerdoti Coen [Mon, 8 Apr 2013 12:20:15 +0000 (12:20 +0000)]
Patch by Paolo Tranquilli. It fixes the following problem: when a new
tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.

11 years agocommit by user andrea
matitaweb [Mon, 8 Apr 2013 11:53:15 +0000 (11:53 +0000)]
commit by user andrea

11 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Sun, 7 Apr 2013 21:38:03 +0000 (21:38 +0000)]
update in basic_2 and apps_2

11 years ago- new component for restricted computation (delta, zeta and tau only)
Ferruccio Guidi [Sun, 7 Apr 2013 21:36:03 +0000 (21:36 +0000)]
- new component for restricted computation (delta, zeta and tau only)
- subclosure preseves native validity asexpected
- some renaming

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 5 Apr 2013 12:25:17 +0000 (12:25 +0000)]
update in basic_2

11 years ago- parallel substitution reaxiomatized
Ferruccio Guidi [Fri, 5 Apr 2013 11:56:45 +0000 (11:56 +0000)]
- parallel substitution reaxiomatized
- supclosure reaxiomatixed (now commutes with parallel substitution)
- some refactoring

11 years ago- probe: recursive removal of empty directories
Ferruccio Guidi [Wed, 20 Mar 2013 18:43:07 +0000 (18:43 +0000)]
- probe: recursive removal of empty directories
- matitadep: improved parsing of input

11 years agomissing or rootless dependences now don't break the compilation process
Ferruccio Guidi [Mon, 18 Mar 2013 21:03:54 +0000 (21:03 +0000)]
missing or rootless dependences now don't break the compilation process

11 years agosome additions
Ferruccio Guidi [Mon, 18 Mar 2013 19:28:47 +0000 (19:28 +0000)]
some additions

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 18 Mar 2013 19:23:53 +0000 (19:23 +0000)]
update in basic_2

11 years agoa file was added by mistake
Ferruccio Guidi [Mon, 18 Mar 2013 19:21:57 +0000 (19:21 +0000)]
a file was added by mistake

11 years ago- more understanding of the "big tree" reduction step
Ferruccio Guidi [Mon, 18 Mar 2013 19:10:19 +0000 (19:10 +0000)]
- more understanding of the "big tree" reduction step

11 years agosfr renamed as lbotr and its symbol changed according to lsubr
Ferruccio Guidi [Sun, 17 Mar 2013 23:31:36 +0000 (23:31 +0000)]
sfr renamed as lbotr and its symbol changed according to lsubr

11 years agonotational change for lsubr:
Ferruccio Guidi [Sun, 17 Mar 2013 19:51:19 +0000 (19:51 +0000)]
notational change for lsubr:
now looks like the other refinements for local environments

11 years agolsubs renamed as lsubr
Ferruccio Guidi [Sun, 17 Mar 2013 17:43:13 +0000 (17:43 +0000)]
lsubs renamed as lsubr

11 years agonotational change for snv and lsubsv: inverted "!" used for now
Ferruccio Guidi [Sun, 17 Mar 2013 15:28:18 +0000 (15:28 +0000)]
notational change for snv and lsubsv: inverted "!" used for now

11 years agomilestone in basic_2!
Ferruccio Guidi [Sat, 16 Mar 2013 22:28:17 +0000 (22:28 +0000)]
milestone in basic_2!

11 years ago- lambdadelta: last recursive part of preservation finally proved!
Ferruccio Guidi [Sat, 16 Mar 2013 22:24:19 +0000 (22:24 +0000)]
- lambdadelta: last recursive part of preservation finally proved!
  some notational changes
- BTM: one file was missing
- probe: now sources and objects not having a .ma file are deleted

11 years agothis is the real update :)
Ferruccio Guidi [Thu, 14 Mar 2013 23:12:55 +0000 (23:12 +0000)]
this is the real update :)

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 14 Mar 2013 23:07:40 +0000 (23:07 +0000)]
update in basic_2

11 years ago- main proof case closed in the 4th component of preservation
Ferruccio Guidi [Thu, 14 Mar 2013 23:06:19 +0000 (23:06 +0000)]
- main proof case closed in the 4th component of preservation
- bug fix in Makefile: now both xoa and probe receive both
configuration files
- useless notion lsubss removed (to be replaced by lsubse)

11 years ago- lambdadelta: third recursive part of preservation finally proved!
Ferruccio Guidi [Wed, 13 Mar 2013 22:11:34 +0000 (22:11 +0000)]
- lambdadelta: third recursive part of preservation finally proved!
  Makefile: xoa.conf passed to probe for future use
- xoa, probe: now can *really* take several configuration files

11 years agomore results on lenv refinement for stratified native validity
Ferruccio Guidi [Mon, 11 Mar 2013 19:29:23 +0000 (19:29 +0000)]
more results on lenv refinement for stratified native validity

11 years agobugfix in web tables
Ferruccio Guidi [Mon, 11 Mar 2013 19:27:07 +0000 (19:27 +0000)]
bugfix in web tables

11 years agosome bugs fixed
Ferruccio Guidi [Mon, 11 Mar 2013 19:21:15 +0000 (19:21 +0000)]
some bugs fixed

11 years ago- xslt and Makefile improved, web pages regenerated
Ferruccio Guidi [Mon, 11 Mar 2013 12:59:19 +0000 (12:59 +0000)]
- xslt and Makefile improved, web pages regenerated

11 years agoChpater 4 and 5
Andrea Asperti [Mon, 11 Mar 2013 10:32:22 +0000 (10:32 +0000)]
Chpater 4 and 5

11 years ago- improved Makefile esp. with the "trim" function
Ferruccio Guidi [Sun, 10 Mar 2013 17:05:30 +0000 (17:05 +0000)]
- improved Makefile esp. with the "trim" function
- some files trimmed

11 years agochapters 2 e 3
Andrea Asperti [Sun, 10 Mar 2013 14:08:14 +0000 (14:08 +0000)]
chapters 2 e 3

11 years agowe removed a useless assertion that was forcing matita to edit just matita files
Ferruccio Guidi [Sun, 10 Mar 2013 12:01:43 +0000 (12:01 +0000)]
we removed a useless assertion that was forcing matita to edit just matita files
matita's editor is good on its own and has interesting facilities including predefined virtuals
in lambdadelta we use matita to edit the .tbl files containing notation from the .ma's
and we use matita as well to edit predefined_virtuals.ml
we still wonder how we could do this up to now despite the assertion!

11 years ago- update in basic_2
Ferruccio Guidi [Sat, 9 Mar 2013 22:32:07 +0000 (22:32 +0000)]
- update in basic_2
- contrib specific web pages moved out
- improved Makefiles

11 years agobasic_2_src.tbl was not updated :(
Ferruccio Guidi [Sat, 9 Mar 2013 22:26:54 +0000 (22:26 +0000)]
basic_2_src.tbl was not updated :(

11 years ago- lenv refinement for stratified native validity redefined
Ferruccio Guidi [Sat, 9 Mar 2013 17:14:31 +0000 (17:14 +0000)]
- lenv refinement for stratified native validity redefined
- contrib specufic web pages moved here

11 years agosecond recursive part of preservation finally proved!
Ferruccio Guidi [Fri, 8 Mar 2013 19:48:14 +0000 (19:48 +0000)]
second recursive part of preservation finally proved!

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 8 Mar 2013 13:47:28 +0000 (13:47 +0000)]
update in basic_2

11 years agoimproved "big treee" computation allows to close a case in the
Ferruccio Guidi [Fri, 8 Mar 2013 13:33:29 +0000 (13:33 +0000)]
improved "big treee" computation allows to close a case in the
preservation proof

11 years agoBug fixed: let-rec defined propositions are no longer extracted.
Claudio Sacerdoti Coen [Mon, 4 Mar 2013 01:31:00 +0000 (01:31 +0000)]
Bug fixed: let-rec defined propositions are no longer extracted.
They used to be extracted, but in the interface the type abstraction was
wrong.

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 3 Mar 2013 18:54:10 +0000 (18:54 +0000)]
update in basic_2

11 years ago- lambdadelta: we removed focalized reduction from snv preservation
Ferruccio Guidi [Sun, 3 Mar 2013 18:52:14 +0000 (18:52 +0000)]
- lambdadelta: we removed focalized reduction from snv preservation
- matitadep: bug fix in loop detection

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 28 Feb 2013 18:15:19 +0000 (18:15 +0000)]
update in basic_2

11 years ago- lambdadelta: first recursive part of preservation finally proved!
Ferruccio Guidi [Thu, 28 Feb 2013 18:14:27 +0000 (18:14 +0000)]
- lambdadelta: first recursive part of preservation finally proved!
- lambda: bugfix in include paths, now they are relative to the root
- matita.lang: keyword "fact" added (used in lambdadelta)

11 years agochapter2 revisited
Andrea Asperti [Thu, 28 Feb 2013 16:22:28 +0000 (16:22 +0000)]
chapter2 revisited

11 years agoQuick patch: the maxmeta is now pushed/popped when compiling an external file.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:19:28 +0000 (20:19 +0000)]
Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.

11 years agoQuick patch: the maxmeta is now pushed/popped when compiling an external file.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:19:04 +0000 (20:19 +0000)]
Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.

11 years agoBug fixed: composite coercions were not extracted.
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:18:18 +0000 (20:18 +0000)]
Bug fixed: composite coercions were not extracted.

11 years agoBug fixed that reveals a new one: in case of inductive types defined via
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 20:17:41 +0000 (20:17 +0000)]
Bug fixed that reveals a new one: in case of inductive types defined via
let rec, it used to happen that a "type 'a foo" in the .mli was implemented
by a "type 'a foo" in the .ml. Now the opposite happens in other situations.

11 years agoFerruccio's removal of objects commented out because it breaks compilation of
Claudio Sacerdoti Coen [Wed, 27 Feb 2013 18:30:24 +0000 (18:30 +0000)]
Ferruccio's removal of objects commented out because it breaks compilation of
the standard library!

11 years agoChapter 1 revisited
Andrea Asperti [Wed, 27 Feb 2013 16:48:15 +0000 (16:48 +0000)]
Chapter 1 revisited

11 years agowhen we serialize the contents of a .ma, we remove the old objects
Ferruccio Guidi [Mon, 25 Feb 2013 21:22:24 +0000 (21:22 +0000)]
when we serialize the contents of a .ma, we remove the old objects
before adding the new ones

11 years ago- xhtbl: now double quotes can appear in string literals
Ferruccio Guidi [Sun, 24 Feb 2013 18:25:57 +0000 (18:25 +0000)]
- xhtbl: now double quotes can appear in string literals
         built-in help completed

11 years ago- nUri : added Sets of uris for use in "probe"
Ferruccio Guidi [Sun, 24 Feb 2013 16:20:34 +0000 (16:20 +0000)]
- nUri : added Sets of uris for use in "probe"
- probe: now we can exclude the objects of dismissed sources
  (those in .matita/ but not in the development as .ma)
- lambdadelta: Makefile now uses the new feature of "probe"

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 22 Feb 2013 21:54:29 +0000 (21:54 +0000)]
update in basic_2

11 years ago- "big tree" order implemented
Ferruccio Guidi [Fri, 22 Feb 2013 21:47:07 +0000 (21:47 +0000)]
- "big tree" order implemented
- some annotations

11 years agotrace added in a failing invocation of auto :-(
Ferruccio Guidi [Mon, 18 Feb 2013 21:50:27 +0000 (21:50 +0000)]
trace added in a failing invocation of auto :-(

11 years agoupdate in basic_2
Ferruccio Guidi [Mon, 18 Feb 2013 19:41:43 +0000 (19:41 +0000)]
update in basic_2

11 years agosubstitution lemma for stratified native validity!
Ferruccio Guidi [Mon, 18 Feb 2013 19:40:13 +0000 (19:40 +0000)]
substitution lemma for stratified native validity!

11 years agoupdate in basic_2 summary
Ferruccio Guidi [Fri, 15 Feb 2013 18:54:16 +0000 (18:54 +0000)]
update in basic_2 summary

11 years agowe rephrased sstas in terms of star
Ferruccio Guidi [Fri, 15 Feb 2013 18:52:30 +0000 (18:52 +0000)]
we rephrased sstas in terms of star

11 years agoupdate in basic_2
Ferruccio Guidi [Fri, 15 Feb 2013 14:21:51 +0000 (14:21 +0000)]
update in basic_2

11 years agowe reformulate the extended computation to simplify the proof of its
Ferruccio Guidi [Fri, 15 Feb 2013 14:17:58 +0000 (14:17 +0000)]
we reformulate the extended computation to simplify the proof of its
normalization property

11 years agostatistics update in basic_2
Ferruccio Guidi [Wed, 13 Feb 2013 15:48:46 +0000 (15:48 +0000)]
statistics update in basic_2

11 years ago- first piece of the mutual induction for preservation finally closed!
Ferruccio Guidi [Wed, 13 Feb 2013 15:41:00 +0000 (15:41 +0000)]
- first piece of the mutual induction for preservation finally closed!
- a conjecture closed

11 years agoan update in basic_2
Ferruccio Guidi [Mon, 11 Feb 2013 22:58:04 +0000 (22:58 +0000)]
an update in basic_2

11 years agomore service lemmas in nat and lambdadelta
Ferruccio Guidi [Mon, 11 Feb 2013 22:56:54 +0000 (22:56 +0000)]
more service lemmas in nat and lambdadelta

11 years agoone table was nissing ...
Ferruccio Guidi [Thu, 7 Feb 2013 19:54:16 +0000 (19:54 +0000)]
one table was nissing ...

11 years agoupdate in basic_2
Ferruccio Guidi [Thu, 7 Feb 2013 19:50:22 +0000 (19:50 +0000)]
update in basic_2

11 years agoeven more service lemmas ...
Ferruccio Guidi [Thu, 7 Feb 2013 18:58:52 +0000 (18:58 +0000)]
even more service lemmas ...

11 years agoA few integrations
Andrea Asperti [Thu, 7 Feb 2013 09:15:07 +0000 (09:15 +0000)]
A few integrations

11 years agorestructuring
Andrea Asperti [Thu, 7 Feb 2013 09:14:39 +0000 (09:14 +0000)]
restructuring

11 years ago(no commit message)
Andrea Asperti [Thu, 7 Feb 2013 09:13:27 +0000 (09:13 +0000)]

11 years agorestructuring
Andrea Asperti [Thu, 7 Feb 2013 09:10:31 +0000 (09:10 +0000)]
restructuring

11 years agoupdate in basic_2
Ferruccio Guidi [Wed, 6 Feb 2013 20:58:01 +0000 (20:58 +0000)]
update in basic_2

11 years ago- lambdadelta: more service lemmas ...
Ferruccio Guidi [Wed, 6 Feb 2013 20:51:46 +0000 (20:51 +0000)]
- lambdadelta: more service lemmas ...
- matitadep: bug fix due to new invocation from Makefile

11 years agosome missing files ...
Ferruccio Guidi [Tue, 5 Feb 2013 17:50:19 +0000 (17:50 +0000)]
some missing files ...

11 years agoBug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
Claudio Sacerdoti Coen [Tue, 5 Feb 2013 13:16:22 +0000 (13:16 +0000)]
Bug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
not active.

11 years agoBug fixed: "open X" were not printed in .mli because streams are destructive.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 22:38:43 +0000 (22:38 +0000)]
Bug fixed: "open X" were not printed in .mli because streams are destructive.

11 years agoFlushing needed before closing the channel.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 22:36:52 +0000 (22:36 +0000)]
Flushing needed before closing the channel.

11 years agoImproved exception handling.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 22:35:57 +0000 (22:35 +0000)]
Improved exception handling.

11 years agoBug fixed in pretty printing of mutual inductive types.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 20:27:04 +0000 (20:27 +0000)]
Bug fixed in pretty printing of mutual inductive types.

11 years agoBug fixed: the indty can be typed with a Prod, not only with a Sort.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 18:09:37 +0000 (18:09 +0000)]
Bug fixed: the indty can be typed with a Prod, not only with a Sort.

11 years agoNew option -extract_ocaml to extract to ocaml files.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 17:38:31 +0000 (17:38 +0000)]
New option -extract_ocaml to extract to ocaml files.

11 years agoPretty printing of ocaml files slightly improved.
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 17:35:10 +0000 (17:35 +0000)]
Pretty printing of ocaml files slightly improved.

11 years agoLast known bug unrelated to names fixed: a fixpoint that creates a type used
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 17:27:38 +0000 (17:27 +0000)]
Last known bug unrelated to names fixed: a fixpoint that creates a type used
to be extracted in the wrong way.

11 years agostate mte2 renamed to mte_acc
Wilmer Ricciotti [Mon, 4 Feb 2013 16:18:55 +0000 (16:18 +0000)]
state mte2 renamed to mte_acc

11 years ago...
Claudio Sacerdoti Coen [Mon, 4 Feb 2013 15:55:41 +0000 (15:55 +0000)]
...

11 years agoconverting certain basic machines to composed machines
Wilmer Ricciotti [Mon, 4 Feb 2013 15:46:19 +0000 (15:46 +0000)]
converting certain basic machines to composed machines

11 years agodefs.ma was never really used
Wilmer Ricciotti [Mon, 4 Feb 2013 11:14:36 +0000 (11:14 +0000)]
defs.ma was never really used

11 years agoMakefile to extract to ocaml code.
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:44:07 +0000 (00:44 +0000)]
Makefile to extract to ocaml code.

11 years agoOops, part of last commit (ocaml extraction implementation)
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:41:54 +0000 (00:41 +0000)]
Oops, part of last commit (ocaml extraction implementation)

11 years agoOoops, this completes the previous commit (ocaml extraction implementation).
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:38:55 +0000 (00:38 +0000)]
Ooops, this completes the previous commit (ocaml extraction implementation).

11 years agoImplementation of Ocaml extraction (largely ported from Coq).
Claudio Sacerdoti Coen [Sat, 2 Feb 2013 00:38:05 +0000 (00:38 +0000)]
Implementation of Ocaml extraction (largely ported from Coq).
Note: yet to be thoroughly debugged.

In order to use, recompile everything with "OCAML_EXTRACTION=1 ocamlc".