]>
matita.cs.unibo.it Git - helm.git/log
Wilmer Ricciotti [Wed, 22 Jun 2011 12:39:51 +0000 (12:39 +0000)]
Second attempt at dialog boxes in index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:28:03 +0000 (12:28 +0000)]
Bugfix in index.html.
Wilmer Ricciotti [Wed, 22 Jun 2011 12:25:51 +0000 (12:25 +0000)]
First attempt at dialog boxes.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:40:54 +0000 (09:40 +0000)]
More bugfixes for matitaweb's viewlib.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:37:31 +0000 (09:37 +0000)]
Bugfix in matitaweb viewlib.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:33:23 +0000 (09:33 +0000)]
Matitaweb viewlib, part II.
Claudio Sacerdoti Coen [Wed, 22 Jun 2011 09:32:36 +0000 (09:32 +0000)]
Escaping exceptions are now captured.
Wilmer Ricciotti [Wed, 22 Jun 2011 09:06:32 +0000 (09:06 +0000)]
Added viewlib to matitaweb.
Ferruccio Guidi [Tue, 21 Jun 2011 20:35:04 +0000 (20:35 +0000)]
missing ; to delimit syntax :(
Wilmer Ricciotti [Tue, 21 Jun 2011 15:31:11 +0000 (15:31 +0000)]
More bugfixes in matitaFilesystem.ml
Wilmer Ricciotti [Tue, 21 Jun 2011 15:19:53 +0000 (15:19 +0000)]
Bugfix in matitaFilesystem.ml
Wilmer Ricciotti [Tue, 21 Jun 2011 15:06:43 +0000 (15:06 +0000)]
Changed user library dir to users/
Wilmer Ricciotti [Tue, 21 Jun 2011 14:58:49 +0000 (14:58 +0000)]
Added generation of HTML representation of the library.
Andrea Asperti [Tue, 21 Jun 2011 13:56:49 +0000 (13:56 +0000)]
Some progress
Andrea Asperti [Mon, 20 Jun 2011 09:16:00 +0000 (09:16 +0000)]
ported reduction.ma
Andrea Asperti [Mon, 20 Jun 2011 08:31:54 +0000 (08:31 +0000)]
Ported par_reduction
Andrea Asperti [Mon, 20 Jun 2011 07:38:34 +0000 (07:38 +0000)]
ported substs and subterms
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
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 11:32:30 +0000 (11:32 +0000)]
Unprotected List.fold_left2.
Claudio Sacerdoti Coen [Fri, 17 Jun 2011 10:22:29 +0000 (10:22 +0000)]
Remove the daemon :-)
Andrea Asperti [Fri, 17 Jun 2011 09:49:27 +0000 (09:49 +0000)]
New syntax of dummy with the type
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
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.
Wilmer Ricciotti [Thu, 16 Jun 2011 14:00:17 +0000 (14:00 +0000)]
Added location of the weblib repository to matita.conf.xml.in.
Wilmer Ricciotti [Thu, 16 Jun 2011 13:53:23 +0000 (13:53 +0000)]
Added repository for the shared library to be used by matitaweb.
Wilmer Ricciotti [Wed, 15 Jun 2011 16:15:09 +0000 (16:15 +0000)]
(Almost) working multi-user matitaweb.
Wilmer Ricciotti [Wed, 15 Jun 2011 14:13:24 +0000 (14:13 +0000)]
Logout (partial work) (multi-user matita)
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.
Ferruccio Guidi [Tue, 14 Jun 2011 19:00:26 +0000 (19:00 +0000)]
some restructuring
Ferruccio Guidi [Tue, 14 Jun 2011 18:24:05 +0000 (18:24 +0000)]
more lemmas to prove and a correction in subst
Ferruccio Guidi [Mon, 13 Jun 2011 17:59:58 +0000 (17:59 +0000)]
more notation and one more lemma to prove :(
Ferruccio Guidi [Mon, 13 Jun 2011 13:12:10 +0000 (13:12 +0000)]
reductions rules and one lemma
Ferruccio Guidi [Sun, 12 Jun 2011 17:25:50 +0000 (17:25 +0000)]
more properties of relocation
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.
Wilmer Ricciotti [Thu, 9 Jun 2011 15:27:04 +0000 (15:27 +0000)]
Fixes bugs in the Matitaweb UI.
Wilmer Ricciotti [Wed, 8 Jun 2011 15:55:47 +0000 (15:55 +0000)]
Fix for internet explorer (but still works badly).
Wilmer Ricciotti [Wed, 8 Jun 2011 15:52:31 +0000 (15:52 +0000)]
Cosmetic changes.
Wilmer Ricciotti [Wed, 8 Jun 2011 12:04:28 +0000 (12:04 +0000)]
Fixed a bug in the retract command of Matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:22:14 +0000 (11:22 +0000)]
Logo for use in matitaweb.
Wilmer Ricciotti [Wed, 8 Jun 2011 11:14:02 +0000 (11:14 +0000)]
Removed dependency of Matitaweb from GTK libraries.
Ferruccio Guidi [Tue, 7 Jun 2011 21:37:47 +0000 (21:37 +0000)]
- we removed the reduction-related item categorization
- some renaming
Wilmer Ricciotti [Tue, 7 Jun 2011 15:12:00 +0000 (15:12 +0000)]
Removed hardcoded include paths from matitadaemon.
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:54 +0000 (14:52 +0000)]
Some changes in the Makefile for matitaweb.
Wilmer Ricciotti [Tue, 7 Jun 2011 14:52:30 +0000 (14:52 +0000)]
Fixes record projections (see matita 1.0 branch)
Wilmer Ricciotti [Tue, 7 Jun 2011 14:36:36 +0000 (14:36 +0000)]
Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd
Claudio Sacerdoti Coen [Tue, 7 Jun 2011 12:13:27 +0000 (12:13 +0000)]
This can happen: when you use nodelta.
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.
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.
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
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.
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.
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
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!
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.
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.
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.
Claudio Sacerdoti Coen [Fri, 3 Jun 2011 08:32:32 +0000 (08:32 +0000)]
Avoid killing the main gui thread.
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....
Ferruccio Guidi [Wed, 1 Jun 2011 14:18:46 +0000 (14:18 +0000)]
CC2FO_K_cube: soundness of the K interpretation stated
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 12:57:28 +0000 (12:57 +0000)]
Comment is now up-to-date.
Wilmer Ricciotti [Wed, 1 Jun 2011 12:29:29 +0000 (12:29 +0000)]
Matita Web: moved the javascript in a separate file. Bugfixes.
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
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 11:34:24 +0000 (11:34 +0000)]
Print backtrace of exceptions when OCAMLRUNPARAM=b is setted.
Claudio Sacerdoti Coen [Wed, 1 Jun 2011 11:27:34 +0000 (11:27 +0000)]
assert false removed
Wilmer Ricciotti [Tue, 31 May 2011 13:59:37 +0000 (13:59 +0000)]
Partial implementation of "go to cursor" action.
Ferruccio Guidi [Mon, 30 May 2011 19:18:51 +0000 (19:18 +0000)]
auto does not work here :(
Ferruccio Guidi [Mon, 30 May 2011 18:34:47 +0000 (18:34 +0000)]
basics: some additions
lambda: some additions + split of lift and subst
Claudio Sacerdoti Coen [Mon, 30 May 2011 16:28:27 +0000 (16:28 +0000)]
Better indentation.
Wilmer Ricciotti [Mon, 30 May 2011 12:25:24 +0000 (12:25 +0000)]
Partially working table layout of matita web (only on some browsers).
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.
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.
Wilmer Ricciotti [Thu, 26 May 2011 14:14:13 +0000 (14:14 +0000)]
Improved rendering of sequents in matitaweb, including handling of multiple
goals.
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)
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
Wilmer Ricciotti [Thu, 26 May 2011 11:48:48 +0000 (11:48 +0000)]
Preliminary version of matitaweb handling multiple goals in the sequent view.
Claudio Sacerdoti Coen [Thu, 26 May 2011 09:33:31 +0000 (09:33 +0000)]
Syntax for coercion nocomposites fixed.
Claudio Sacerdoti Coen [Thu, 26 May 2011 09:27:38 +0000 (09:27 +0000)]
Added "nocomposites" to coercions.
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)
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.
Claudio Sacerdoti Coen [Tue, 24 May 2011 21:39:32 +0000 (21:39 +0000)]
Coercions are now propagated under let...ins.
Wilmer Ricciotti [Tue, 24 May 2011 16:40:35 +0000 (16:40 +0000)]
Fixed box pretty printing.
Wilmer Ricciotti [Tue, 24 May 2011 13:24:53 +0000 (13:24 +0000)]
matitaweb: added retract (undo)
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
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
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.
Wilmer Ricciotti [Mon, 23 May 2011 10:49:02 +0000 (10:49 +0000)]
...
Andrea Asperti [Mon, 23 May 2011 10:24:12 +0000 (10:24 +0000)]
Removed dead code
Ferruccio Guidi [Fri, 20 May 2011 14:35:59 +0000 (14:35 +0000)]
- we weakened SAT3
- we simplified the specifications of the Cube
Andrea Asperti [Fri, 20 May 2011 10:34:09 +0000 (10:34 +0000)]
want_indent bug fixed
Andrea Asperti [Fri, 20 May 2011 10:06:00 +0000 (10:06 +0000)]
readded function box_of
Wilmer Ricciotti [Fri, 20 May 2011 09:59:53 +0000 (09:59 +0000)]
Compilation fix
Wilmer Ricciotti [Fri, 20 May 2011 09:59:31 +0000 (09:59 +0000)]
Compilation fix
Andrea Asperti [Fri, 20 May 2011 08:50:16 +0000 (08:50 +0000)]
Simplified rendering.
Andrea Asperti [Fri, 20 May 2011 08:49:10 +0000 (08:49 +0000)]
Simplified rendering
Andrea Asperti [Fri, 20 May 2011 08:48:27 +0000 (08:48 +0000)]
Simplified rendering
Andrea Asperti [Fri, 20 May 2011 08:45:36 +0000 (08:45 +0000)]
rm rendering attrs
Andrea Asperti [Fri, 20 May 2011 08:44:09 +0000 (08:44 +0000)]
Removed mathml and proof rendering.
Andrea Asperti [Fri, 20 May 2011 08:42:04 +0000 (08:42 +0000)]
Simplified rendering
Andrea Asperti [Fri, 20 May 2011 08:34:57 +0000 (08:34 +0000)]
Porting to new reduction.
Wilmer Ricciotti [Thu, 19 May 2011 14:14:06 +0000 (14:14 +0000)]
Added matitadaemon.