]> matita.cs.unibo.it Git - helm.git/log
helm.git
13 years agoAdded generation of HTML representation of the library.
Wilmer Ricciotti [Tue, 21 Jun 2011 14:58:49 +0000 (14:58 +0000)]
Added generation of HTML representation of the library.

13 years agoSome progress
Andrea Asperti [Tue, 21 Jun 2011 13:56:49 +0000 (13:56 +0000)]
Some progress

13 years agoported reduction.ma
Andrea Asperti [Mon, 20 Jun 2011 09:16:00 +0000 (09:16 +0000)]
ported reduction.ma

13 years agoPorted par_reduction
Andrea Asperti [Mon, 20 Jun 2011 08:31:54 +0000 (08:31 +0000)]
Ported par_reduction

13 years agoported substs and subterms
Andrea Asperti [Mon, 20 Jun 2011 07:38:34 +0000 (07:38 +0000)]
ported substs and subterms

13 years ago- xoa: more existential types
Ferruccio Guidi [Sat, 18 Jun 2011 14:29:50 +0000 (14:29 +0000)]
- xoa: more existential types
- ground: more arithmetics
- lift: more nasic inversion lemmas and some renaming

13 years agoUnprotected List.fold_left2.
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 11:32:30 +0000 (11:32 +0000)]
Unprotected List.fold_left2.

13 years agoRemove the daemon :-)
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 10:22:29 +0000 (10:22 +0000)]
Remove the daemon :-)

13 years agoNew syntax of dummy with the type
Andrea Asperti [Fri, 17 Jun 2011 09:49:27 +0000 (09:49 +0000)]
New syntax of dummy with the type

13 years agoAdded a copy of lambdaN to extend the syntax of dummies with types
Andrea Asperti [Fri, 17 Jun 2011 09:01:29 +0000 (09:01 +0000)]
Added a copy of lambdaN to extend the syntax of dummies with types

13 years agoAdded module MatitaFilesystem, to be used for the management of the library
Wilmer Ricciotti [Thu, 16 Jun 2011 14:52:19 +0000 (14:52 +0000)]
Added module MatitaFilesystem, to be used for the management of the library
in matitaweb.

13 years agoAdded location of the weblib repository to matita.conf.xml.in.
Wilmer Ricciotti [Thu, 16 Jun 2011 14:00:17 +0000 (14:00 +0000)]
Added location of the weblib repository to matita.conf.xml.in.

13 years agoAdded repository for the shared library to be used by matitaweb.
Wilmer Ricciotti [Thu, 16 Jun 2011 13:53:23 +0000 (13:53 +0000)]
Added repository for the shared library to be used by matitaweb.

13 years ago(Almost) working multi-user matitaweb.
Wilmer Ricciotti [Wed, 15 Jun 2011 16:15:09 +0000 (16:15 +0000)]
(Almost) working multi-user matitaweb.

13 years agoLogout (partial work) (multi-user matita)
Wilmer Ricciotti [Wed, 15 Jun 2011 14:13:24 +0000 (14:13 +0000)]
Logout (partial work) (multi-user matita)

13 years agoMulti-user Matita (and Matitaweb): added user authentication (currently only
Wilmer Ricciotti [Wed, 15 Jun 2011 12:49:01 +0000 (12:49 +0000)]
Multi-user Matita (and Matitaweb): added user authentication (currently only
tested on hard-coded accounts). Proof-objects are saved in a user-specific
directory.

13 years agosome restructuring
Ferruccio Guidi [Tue, 14 Jun 2011 19:00:26 +0000 (19:00 +0000)]
some restructuring

13 years agomore lemmas to prove and a correction in subst
Ferruccio Guidi [Tue, 14 Jun 2011 18:24:05 +0000 (18:24 +0000)]
more lemmas to prove and a correction in subst

13 years agomore notation and one more lemma to prove :(
Ferruccio Guidi [Mon, 13 Jun 2011 17:59:58 +0000 (17:59 +0000)]
more notation and one more lemma to prove :(

13 years agoreductions rules and one lemma
Ferruccio Guidi [Mon, 13 Jun 2011 13:12:10 +0000 (13:12 +0000)]
reductions rules and one lemma

13 years agomore properties of relocation
Ferruccio Guidi [Sun, 12 Jun 2011 17:25:50 +0000 (17:25 +0000)]
more properties of relocation

13 years agoMulti-user matita: changed the status object to include a ``user'' method
Wilmer Ricciotti [Fri, 10 Jun 2011 12:56:04 +0000 (12:56 +0000)]
Multi-user matita: changed the status object to include a ``user'' method
containing an optional string, used to identify associated user.

13 years agoFixes bugs in the Matitaweb UI.
Wilmer Ricciotti [Thu, 9 Jun 2011 15:27:04 +0000 (15:27 +0000)]
Fixes bugs in the  Matitaweb UI.

13 years agoFix for internet explorer (but still works badly).
Wilmer Ricciotti [Wed, 8 Jun 2011 15:55:47 +0000 (15:55 +0000)]
Fix for internet explorer (but still works badly).

13 years agoCosmetic changes.
Wilmer Ricciotti [Wed, 8 Jun 2011 15:52:31 +0000 (15:52 +0000)]
Cosmetic changes.

13 years agoFixed a bug in the retract command of Matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 12:04:28 +0000 (12:04 +0000)]
Fixed a bug in the retract command of Matitaweb.

13 years agoLogo for use in matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:22:14 +0000 (11:22 +0000)]
Logo for use in matitaweb.

13 years agoRemoved dependency of Matitaweb from GTK libraries.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:14:02 +0000 (11:14 +0000)]
Removed dependency of Matitaweb from GTK libraries.

13 years ago- we removed the reduction-related item categorization
Ferruccio Guidi [Tue, 7 Jun 2011 21:37:47 +0000 (21:37 +0000)]
- we removed the reduction-related item categorization
- some renaming

13 years agoRemoved hardcoded include paths from matitadaemon.
Wilmer Ricciotti [Tue, 7 Jun 2011 15:12:00 +0000 (15:12 +0000)]
Removed hardcoded include paths from matitadaemon.

13 years agoSome changes in the Makefile for matitaweb.
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:54 +0000 (14:52 +0000)]
Some changes in the Makefile for matitaweb.

13 years agoFixes record projections (see matita 1.0 branch)
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:30 +0000 (14:52 +0000)]
Fixes record projections (see matita 1.0 branch)

13 years agoMatitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd
Wilmer Ricciotti [Tue, 7 Jun 2011 14:36:36 +0000 (14:36 +0000)]
Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd

13 years agoThis can happen: when you use nodelta.
Claudio Sacerdoti Coen [Tue, 7 Jun 2011 12:13:27 +0000 (12:13 +0000)]
This can happen: when you use nodelta.

13 years agoMinor changes because of the new, weaker (but much faster) delift.
Claudio Sacerdoti Coen [Mon, 6 Jun 2011 21:46:32 +0000 (21:46 +0000)]
Minor changes because of the new, weaker (but much faster) delift.

13 years agoBug fixed: trailing ' in names were not removed when computing the next free
Claudio Sacerdoti Coen [Mon, 6 Jun 2011 20:52:43 +0000 (20:52 +0000)]
Bug fixed: trailing ' in names were not removed when computing the next free
name.

13 years agoWe reintroduce the distinction between binding and non-binding items.
Ferruccio Guidi [Mon, 6 Jun 2011 17:19:30 +0000 (17:19 +0000)]
We reintroduce the distinction between binding and non-binding items.
Mon-binding items are now forbidden in environments

13 years agoMajor speed-up:
Claudio Sacerdoti Coen [Mon, 6 Jun 2011 16:41:34 +0000 (16:41 +0000)]
Major speed-up:

 1) bug fixed: the fo_unif applied to a metavariable in the subst made a
    recursive call using unify. Thus, in case of failure of the unify
    (after hints, reduction, etc.), fo_unif failed and hints, reduction,
    etc. was tried again. This resulted in an exponential blow-up in the
    worst case.
 2) bug fixed: in the case  ? args == ?pattern, the ?pattern was delifted
    w.r.t. args, but during the delift the special unification case with
    a pattern was considered again. This was costly since reduction was
    used on the first argument of the unification.
 3) semantics of fo_unif "fixed": it is now succesfull on every pair of
    terms whose rigid prefix is equal and whose arguments are unifiable.
    Before it used to fail for example on (x args == x args) where x is
    a Rel.
 4) BEHAVIOUR OF DELIFT CHANGED: it no longer matches terms in the local
    context up to full unification, but only up to fo_unif. Some tactics
    that used to be accepted could now fail and the user needs to change
    the terms by hand before applying the tactic. On the other hand, the
    speed up is really significant.

13 years agoThis update uses XML for client-server communication. For unknown reasons, this
Wilmer Ricciotti [Mon, 6 Jun 2011 14:55:54 +0000 (14:55 +0000)]
This update uses XML for client-server communication. For unknown reasons, this
doesn't seem to work well with Firefox (but works ok on Chrome).

We reverted to a single process http daemon because of an annoying bug in
Ocaml Http, causing the daemon to terminate randomly.

13 years ago- we introduce extended existentials (generated)
Ferruccio Guidi [Fri, 3 Jun 2011 16:52:50 +0000 (16:52 +0000)]
- we introduce extended existentials (generated)
- we exploit the tactic "*" to reduce the volume of decompositions

13 years agoMax width overflows, which cause auto to fail, are now logged as errors.
Ferruccio Guidi [Fri, 3 Jun 2011 13:40:38 +0000 (13:40 +0000)]
Max width overflows, which cause auto to fail, are now logged as errors.
The message "auto gave up" is not very informative by itself!

13 years agoFixed a bug that prevented record projections from being generated. This patch
Wilmer Ricciotti [Fri, 3 Jun 2011 09:28:29 +0000 (09:28 +0000)]
Fixed a bug that prevented record projections from being generated. This patch
supersedes a previous one (r11250), which created more problems than those it
solved.

13 years agoThe pretty printer should never fail, even on fake inductive types used in
Claudio Sacerdoti Coen [Fri, 3 Jun 2011 08:55:01 +0000 (08:55 +0000)]
The pretty printer should never fail, even on fake inductive types used in
patterns.

13 years agoPretty printing of exceptions escaped from pretty printing of exceptions
Claudio Sacerdoti Coen [Fri, 3 Jun 2011 08:53:47 +0000 (08:53 +0000)]
Pretty printing of exceptions escaped from pretty printing of exceptions
improved.

13 years agoAvoid killing the main gui thread.
Claudio Sacerdoti Coen [Fri, 3 Jun 2011 08:32:32 +0000 (08:32 +0000)]
Avoid killing the main gui thread.

13 years agoDelift used to produce not well typed substitutions. In turn, this
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 16:36:13 +0000 (16:36 +0000)]
Delift used to produce not well typed substitutions. In turn, this
led to tactics that were not failing immediately, but only at Qed.

Fixed by adding the appropriate check to the delift function.

Note:
 - pass the metavariable number (-1) to avoid the check when you know what
   you are doing (e.g. when delift is just used to restrict a term or to
   replace a term with a convertible one). This used to be 0 (not -1).
 - in some cases (algebraic universes and implicits used to stop chains of
   metavariables) the check is relaxed
 - to make the CerCo script pass (in very "reasonable" and "frequent" cases),
   the algorithm needs to solve the following unification problem:
     S (?[n]) == ?[(S n)]
   Our algorithm used to delift S(?[n]) w.r.t. (S n), yielding x |- ? := x.
   By chance, this was the right solution since S (?[n]) becomes (S n) and
   also ?[(S n)] becomes (S n). However, the two solutions were both added
   to the subst (first bug) and they could even be different (second bug).
   We fix this by checking that they are not different.
   However, at the moment, the solution still occurs twice in the subst....

13 years agoCC2FO_K_cube: soundness of the K interpretation stated
Ferruccio Guidi [Wed, 1 Jun 2011 14:18:46 +0000 (14:18 +0000)]
CC2FO_K_cube: soundness of the K interpretation stated

13 years agoComment is now up-to-date.
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 12:57:28 +0000 (12:57 +0000)]
Comment is now up-to-date.

13 years agoMatita Web: moved the javascript in a separate file. Bugfixes.
Wilmer Ricciotti [Wed, 1 Jun 2011 12:29:29 +0000 (12:29 +0000)]
Matita Web: moved the javascript in a separate file. Bugfixes.

13 years agosubst.ma: some additions
Ferruccio Guidi [Wed, 1 Jun 2011 11:55:11 +0000 (11:55 +0000)]
subst.ma: some additions
convertibility.ma: non "conv" refers to the correct predicate
CC2FO_K.ma: CC to Fomega: first interpretation: substitution lemma

13 years agoPrint backtrace of exceptions when OCAMLRUNPARAM=b is setted.
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 11:34:24 +0000 (11:34 +0000)]
Print backtrace of exceptions when OCAMLRUNPARAM=b is setted.

13 years agoassert false removed
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 11:27:34 +0000 (11:27 +0000)]
assert false removed

13 years agoPartial implementation of "go to cursor" action.
Wilmer Ricciotti [Tue, 31 May 2011 13:59:37 +0000 (13:59 +0000)]
Partial implementation of "go to cursor" action.

13 years agoauto does not work here :(
Ferruccio Guidi [Mon, 30 May 2011 19:18:51 +0000 (19:18 +0000)]
auto does not work here :(

13 years agobasics: some additions
Ferruccio Guidi [Mon, 30 May 2011 18:34:47 +0000 (18:34 +0000)]
basics: some additions
lambda: some additions + split of lift and subst

13 years agoBetter indentation.
Claudio Sacerdoti Coen [Mon, 30 May 2011 16:28:27 +0000 (16:28 +0000)]
Better indentation.

13 years agoPartially working table layout of matita web (only on some browsers).
Wilmer Ricciotti [Mon, 30 May 2011 12:25:24 +0000 (12:25 +0000)]
Partially working table layout of matita web (only on some browsers).

13 years agoDebugging code to understand cases where the output notation is not
Claudio Sacerdoti Coen [Mon, 30 May 2011 11:02:26 +0000 (11:02 +0000)]
Debugging code to understand cases where the output notation is not
applied, is applied badly or it raises an assert failure.

Usually the problem is given by optional parts of the term. For instance,
in output all typing information is present and it _must_ be matched.

13 years agoName generator for Russell greatly improved.
Claudio Sacerdoti Coen [Fri, 27 May 2011 14:58:10 +0000 (14:58 +0000)]
Name generator for Russell greatly improved.
But maybe we need a longer term solution.

13 years agoImproved rendering of sequents in matitaweb, including handling of multiple
Wilmer Ricciotti [Thu, 26 May 2011 14:14:13 +0000 (14:14 +0000)]
Improved rendering of sequents in matitaweb, including handling of multiple
goals.

13 years agoSerious bug fixed:
Claudio Sacerdoti Coen [Thu, 26 May 2011 12:06:11 +0000 (12:06 +0000)]
Serious bug fixed:
 - in order to look for coercions to sort and funclass, we passed
   types containing implicits and a flag to avoid unification
 - totally avoiding unification, it happened
    1) that we diverged:
       t : A :> B ==> inject t : Sigma x.A :> B ==> eject (inject t): A :> B
    2) that we called unification on types that contained implicits
       (in some cases)

13 years agoProd indexed as Dead, that is equal only to itself, instead of Variable that
Enrico Tassi [Thu, 26 May 2011 11:57:17 +0000 (11:57 +0000)]
Prod indexed as Dead, that is equal only to itself, instead of Variable that
is equal to anything

13 years agoPreliminary version of matitaweb handling multiple goals in the sequent view.
Wilmer Ricciotti [Thu, 26 May 2011 11:48:48 +0000 (11:48 +0000)]
Preliminary version of matitaweb handling multiple goals in the sequent view.

13 years agoSyntax for coercion nocomposites fixed.
Claudio Sacerdoti Coen [Thu, 26 May 2011 09:33:31 +0000 (09:33 +0000)]
Syntax for coercion nocomposites fixed.

13 years agoAdded "nocomposites" to coercions.
Claudio Sacerdoti Coen [Thu, 26 May 2011 09:27:38 +0000 (09:27 +0000)]
Added "nocomposites" to coercions.

13 years ago- degree: some improvements and the Deg_append lemma
Ferruccio Guidi [Wed, 25 May 2011 12:22:16 +0000 (12:22 +0000)]
- degree: some improvements and the Deg_append lemma
- lambda_notation: the K interpretation (CC to Fomega mapping)

13 years agoQuick patch to avoid name collisions when passing coercions under let...ins.
Claudio Sacerdoti Coen [Tue, 24 May 2011 22:01:19 +0000 (22:01 +0000)]
Quick patch to avoid name collisions when passing coercions under let...ins.

13 years agoCoercions are now propagated under let...ins.
Claudio Sacerdoti Coen [Tue, 24 May 2011 21:39:32 +0000 (21:39 +0000)]
Coercions are now propagated under let...ins.

13 years agoFixed box pretty printing.
Wilmer Ricciotti [Tue, 24 May 2011 16:40:35 +0000 (16:40 +0000)]
Fixed box pretty printing.

13 years agomatitaweb: added retract (undo)
Wilmer Ricciotti [Tue, 24 May 2011 13:24:53 +0000 (13:24 +0000)]
matitaweb: added retract (undo)

13 years agodegree.ma: we defined the "degree" of a term, which is meaningful in
Ferruccio Guidi [Tue, 24 May 2011 12:19:11 +0000 (12:19 +0000)]
degree.ma: we defined the "degree" of a term, which is meaningful in
the lambda-cube

13 years ago1) interpretation of matches in patterns implemented
Claudio Sacerdoti Coen [Mon, 23 May 2011 23:08:04 +0000 (23:08 +0000)]
1) interpretation of matches in patterns implemented
2) missing exception added to matitaExcPp

13 years agoAdded support for hyperlinks in the goal view of the web interface.
Wilmer Ricciotti [Mon, 23 May 2011 15:13:38 +0000 (15:13 +0000)]
Added support for hyperlinks in the goal view of the web interface.

13 years ago...
Wilmer Ricciotti [Mon, 23 May 2011 10:49:02 +0000 (10:49 +0000)]
...

13 years agoRemoved dead code
Andrea Asperti [Mon, 23 May 2011 10:24:12 +0000 (10:24 +0000)]
Removed dead code

13 years ago- we weakened SAT3
Ferruccio Guidi [Fri, 20 May 2011 14:35:59 +0000 (14:35 +0000)]
- we weakened SAT3
- we simplified the specifications of the Cube

13 years agowant_indent bug fixed
Andrea Asperti [Fri, 20 May 2011 10:34:09 +0000 (10:34 +0000)]
want_indent bug fixed

13 years agoreadded function box_of
Andrea Asperti [Fri, 20 May 2011 10:06:00 +0000 (10:06 +0000)]
readded function box_of

13 years agoCompilation fix
Wilmer Ricciotti [Fri, 20 May 2011 09:59:53 +0000 (09:59 +0000)]
Compilation fix

13 years agoCompilation fix
Wilmer Ricciotti [Fri, 20 May 2011 09:59:31 +0000 (09:59 +0000)]
Compilation fix

13 years agoSimplified rendering.
Andrea Asperti [Fri, 20 May 2011 08:50:16 +0000 (08:50 +0000)]
Simplified rendering.

13 years agoSimplified rendering
Andrea Asperti [Fri, 20 May 2011 08:49:10 +0000 (08:49 +0000)]
Simplified rendering

13 years agoSimplified rendering
Andrea Asperti [Fri, 20 May 2011 08:48:27 +0000 (08:48 +0000)]
Simplified rendering

13 years agorm rendering attrs
Andrea Asperti [Fri, 20 May 2011 08:45:36 +0000 (08:45 +0000)]
rm rendering attrs

13 years agoRemoved mathml and proof rendering.
Andrea Asperti [Fri, 20 May 2011 08:44:09 +0000 (08:44 +0000)]
Removed mathml and proof rendering.

13 years agoSimplified rendering
Andrea Asperti [Fri, 20 May 2011 08:42:04 +0000 (08:42 +0000)]
Simplified rendering

13 years agoPorting to new reduction.
Andrea Asperti [Fri, 20 May 2011 08:34:57 +0000 (08:34 +0000)]
Porting to new reduction.

13 years agoAdded matitadaemon.
Wilmer Ricciotti [Thu, 19 May 2011 14:14:06 +0000 (14:14 +0000)]
Added matitadaemon.

13 years agocube.ma: some pts specifications of the lambda-cube
Ferruccio Guidi [Thu, 19 May 2011 14:12:22 +0000 (14:12 +0000)]
cube.ma: some pts specifications of the lambda-cube

13 years agoPorting to the new pts.
Andrea Asperti [Thu, 19 May 2011 10:36:25 +0000 (10:36 +0000)]
Porting to the new pts.

13 years agoPorting to new parametric TJ.
Andrea Asperti [Thu, 19 May 2011 10:16:44 +0000 (10:16 +0000)]
Porting to new parametric TJ.

13 years agoDummies are blocked.
Andrea Asperti [Thu, 19 May 2011 09:58:04 +0000 (09:58 +0000)]
Dummies are blocked.

13 years agoNew version of TJ parametric in the specification of pts.
Andrea Asperti [Wed, 18 May 2011 09:46:17 +0000 (09:46 +0000)]
New version of TJ parametric in the specification of pts.

13 years agowe added a property
Ferruccio Guidi [Sat, 14 May 2011 18:59:20 +0000 (18:59 +0000)]
we added a property

13 years agoground: some arithmetical properties added
Ferruccio Guidi [Fri, 13 May 2011 21:19:34 +0000 (21:19 +0000)]
ground: some arithmetical properties added
lift: some properties proved

13 years agointerim version (added smallLexer)
Wilmer Ricciotti [Fri, 13 May 2011 08:55:12 +0000 (08:55 +0000)]
interim version (added smallLexer)

13 years agoRecord projections:
Wilmer Ricciotti [Thu, 12 May 2011 16:03:08 +0000 (16:03 +0000)]
Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

13 years agoRecord projections:
Wilmer Ricciotti [Thu, 12 May 2011 15:59:10 +0000 (15:59 +0000)]
Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

13 years agoPartial modifications.
Andrea Asperti [Wed, 11 May 2011 13:26:18 +0000 (13:26 +0000)]
Partial modifications.

13 years agowe uncommented R3 and R4 tu be used in lambda-delta
Ferruccio Guidi [Thu, 28 Apr 2011 15:24:48 +0000 (15:24 +0000)]
we uncommented R3 and R4 tu be used in lambda-delta