]> matita.cs.unibo.it Git - helm.git/log
helm.git
13 years agoMatitaweb: commit test.
Wilmer Ricciotti [Mon, 3 Oct 2011 13:49:18 +0000 (13:49 +0000)]
Matitaweb: commit test.

13 years agoMatitaweb: commit test.
Wilmer Ricciotti [Mon, 3 Oct 2011 13:48:09 +0000 (13:48 +0000)]
Matitaweb: commit test.

13 years agoMatitaweb: commit test.
Wilmer Ricciotti [Mon, 3 Oct 2011 13:46:16 +0000 (13:46 +0000)]
Matitaweb: commit test.

13 years agocommit by user andrea
matitaweb [Mon, 3 Oct 2011 11:04:53 +0000 (11:04 +0000)]
commit by user andrea

13 years agoMatitaweb: implementation of file-flagging for keeping track of modified files
Wilmer Ricciotti [Mon, 3 Oct 2011 10:53:01 +0000 (10:53 +0000)]
Matitaweb: implementation of file-flagging for keeping track of modified files
proceeds.

13 years agonew version
matitaweb [Mon, 3 Oct 2011 10:42:28 +0000 (10:42 +0000)]
new version

13 years agocommit by user andrea
matitaweb [Mon, 3 Oct 2011 10:16:02 +0000 (10:16 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 3 Oct 2011 10:08:06 +0000 (10:08 +0000)]
commit by user andrea

13 years agoMatitaweb file flag test.
matitaweb [Mon, 3 Oct 2011 09:32:48 +0000 (09:32 +0000)]
Matitaweb file flag test.

13 years agocommit by user andrea
matitaweb [Mon, 3 Oct 2011 09:29:37 +0000 (09:29 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 3 Oct 2011 08:15:18 +0000 (08:15 +0000)]
commit by user andrea

13 years ago- xhtbl.css is ready!
Ferruccio Guidi [Sun, 2 Oct 2011 20:52:52 +0000 (20:52 +0000)]
- xhtbl.css is ready!
- images ar now in a dedicated directory

13 years agoMatitaweb: test commit.
matitaweb [Fri, 30 Sep 2011 16:28:42 +0000 (16:28 +0000)]
Matitaweb: test commit.

13 years agoMatitaweb: test commit.
matitaweb [Fri, 30 Sep 2011 16:25:59 +0000 (16:25 +0000)]
Matitaweb: test commit.

13 years agoMatitaweb: test commit.
matitaweb [Fri, 30 Sep 2011 16:21:49 +0000 (16:21 +0000)]
Matitaweb: test commit.

13 years agoMatitaweb: test commit.
matitaweb [Fri, 30 Sep 2011 16:06:36 +0000 (16:06 +0000)]
Matitaweb: test commit.

13 years agoMatitaweb: Library test.
Wilmer Ricciotti [Fri, 30 Sep 2011 16:04:43 +0000 (16:04 +0000)]
Matitaweb: Library test.

13 years ago...
matitaweb [Fri, 30 Sep 2011 16:00:58 +0000 (16:00 +0000)]
...

13 years agoMatitaweb: Some bugfixes concerning file flags.
Wilmer Ricciotti [Fri, 30 Sep 2011 12:38:25 +0000 (12:38 +0000)]
Matitaweb: Some bugfixes concerning file flags.

13 years agoMatitaweb:
matitaweb [Fri, 30 Sep 2011 11:11:22 +0000 (11:11 +0000)]
Matitaweb:
1) Added experimental update functionality
2) Flagged library files -synchronized, modified, conflicted, unmanaged-
   (partial implementation)
3) Various cosmetic changes

13 years agostill new colors ...
Ferruccio Guidi [Thu, 29 Sep 2011 20:27:55 +0000 (20:27 +0000)]
still new colors ...

13 years agobugfix in one of the new colors :)
Ferruccio Guidi [Thu, 29 Sep 2011 20:09:19 +0000 (20:09 +0000)]
bugfix in one of the new colors :)

13 years agobugfix in remote update
Ferruccio Guidi [Thu, 29 Sep 2011 19:57:26 +0000 (19:57 +0000)]
bugfix in remote update

13 years agonew colors for the crux ...
Ferruccio Guidi [Thu, 29 Sep 2011 19:49:44 +0000 (19:49 +0000)]
new colors for the crux ...

13 years agoTutorial update.
matitaweb [Thu, 29 Sep 2011 13:37:58 +0000 (13:37 +0000)]
Tutorial update.

13 years agoTutorial di Matita (lupo, capra, cavoli)
matitaweb [Thu, 29 Sep 2011 12:48:14 +0000 (12:48 +0000)]
Tutorial di Matita (lupo, capra, cavoli)

13 years agoNot well understood patch: an assert false did occur, so I changed it to a
Claudio Sacerdoti Coen [Mon, 26 Sep 2011 12:24:20 +0000 (12:24 +0000)]
Not well understood patch: an assert false did occur, so I changed it to a
pattern matching failure. However, I do not know if this was due to a badly
defined notation or not.

13 years ago- the confluence of context-senstitive parallel reduction (cpr) is closed!
Ferruccio Guidi [Thu, 22 Sep 2011 12:25:07 +0000 (12:25 +0000)]
- the confluence of context-senstitive parallel reduction (cpr) is closed!
- the theory of partial unfold on local environments (ltpss) is set up

13 years agoMatitaweb: Fixed a bug which caused matita to forget the baseuri of the current
Wilmer Ricciotti [Thu, 22 Sep 2011 11:37:36 +0000 (11:37 +0000)]
Matitaweb: Fixed a bug which caused matita to forget the baseuri of the current
script when retracting to the top.

13 years agoMap in NCicUtils now takes an optional boolea to disable head beta reduction.
Andrea Asperti [Wed, 21 Sep 2011 15:51:06 +0000 (15:51 +0000)]
Map in NCicUtils now takes an optional boolea to disable head beta reduction.
We normalize cic terms in the paramodulation blob by stripping out names in
binders.

13 years ago1) removed many debug prints
matitaweb [Wed, 21 Sep 2011 14:56:17 +0000 (14:56 +0000)]
1) removed many debug prints
2) solved a bug in automation (we had forgotten to saturate clauses in
forward_infer_step, a mistake that prevented equations from being
indexed, resulting in almost certain failure of automation).
3) disabled alpha_eq in NCicBlob.compare, because it now requires a
status containing the correct environment, which can't be guessed
inside compare (enabling alpha_eq results in the automation
sporadically failing).

13 years agoMatitaweb: disabled many verbose debug prints.
Wilmer Ricciotti [Tue, 20 Sep 2011 14:52:42 +0000 (14:52 +0000)]
Matitaweb: disabled many verbose debug prints.

13 years agoThe Blob is not abstracted on the context any more.
Andrea Asperti [Tue, 20 Sep 2011 14:00:34 +0000 (14:00 +0000)]
The Blob is not abstracted on the context any more.
The saturate function (that requires the environment now
contained in the status) is now external to the module.
It is defined in NCicBlob.
The functions mk_passive and mk_goals are now expecting
input terms already saturated.

13 years agosome improvements about the partial unfold on terms (tpss)
Ferruccio Guidi [Sun, 18 Sep 2011 21:31:37 +0000 (21:31 +0000)]
some improvements about the partial unfold on terms (tpss)

13 years agoFixes a bug (introduced in the previous revision) which caused the environment
Wilmer Ricciotti [Sat, 17 Sep 2011 00:04:27 +0000 (00:04 +0000)]
Fixes a bug (introduced in the previous revision) which caused the environment
to forget its status.

13 years agoThis commit patches the environment and the library so that their status is
Wilmer Ricciotti [Fri, 16 Sep 2011 14:14:15 +0000 (14:14 +0000)]
This commit patches the environment and the library so that their status is
contained in the global status of Matita. This allows several users to execute
concurrently in the same instance of Matita, since they are now using
independent statuses.

13 years agoFile uploading
matitaweb [Fri, 16 Sep 2011 13:18:56 +0000 (13:18 +0000)]
File uploading

13 years agomah...
matitaweb [Fri, 16 Sep 2011 12:17:47 +0000 (12:17 +0000)]
mah...

13 years agoThe tutorial on line.
matitaweb [Fri, 16 Sep 2011 12:08:28 +0000 (12:08 +0000)]
The tutorial on line.

13 years agoThe tutorial on line
matitaweb [Fri, 16 Sep 2011 12:01:05 +0000 (12:01 +0000)]
The tutorial on line

13 years agounfold on terms completed!
Ferruccio Guidi [Thu, 15 Sep 2011 21:43:51 +0000 (21:43 +0000)]
unfold on terms completed!

13 years agoremote update by make
Ferruccio Guidi [Mon, 12 Sep 2011 15:35:16 +0000 (15:35 +0000)]
remote update by make

13 years agoadded a pointer to helena in Wiedijk's list
Ferruccio Guidi [Mon, 12 Sep 2011 14:39:02 +0000 (14:39 +0000)]
added a pointer to helena in Wiedijk's list

13 years agoupdate
Ferruccio Guidi [Mon, 12 Sep 2011 14:33:06 +0000 (14:33 +0000)]
update

13 years agoAdded debug print in NCicLibrary.serialize.
Wilmer Ricciotti [Mon, 12 Sep 2011 13:00:54 +0000 (13:00 +0000)]
Added debug print in NCicLibrary.serialize.

13 years agobug fix in xslt: missing ld namespace
Ferruccio Guidi [Mon, 12 Sep 2011 12:03:12 +0000 (12:03 +0000)]
bug fix in xslt: missing ld namespace

13 years agorefactoring completed!
Ferruccio Guidi [Mon, 12 Sep 2011 12:00:49 +0000 (12:00 +0000)]
refactoring completed!

13 years agocommit by user utente1
matitaweb [Mon, 12 Sep 2011 11:36:38 +0000 (11:36 +0000)]
commit by user utente1

13 years agobug fix in the dtd
Ferruccio Guidi [Sun, 11 Sep 2011 19:08:29 +0000 (19:08 +0000)]
bug fix in the dtd

13 years agorefactoring and regeneration of lddl
Ferruccio Guidi [Sun, 11 Sep 2011 18:51:41 +0000 (18:51 +0000)]
refactoring and regeneration of lddl

13 years agothe refactoring continues ...
Ferruccio Guidi [Sun, 11 Sep 2011 14:03:37 +0000 (14:03 +0000)]
the refactoring continues ...

13 years agorefactoring ...
Ferruccio Guidi [Sun, 11 Sep 2011 11:20:49 +0000 (11:20 +0000)]
refactoring ...

13 years agoMatitaweb: layout change in the matitaweb inteface, in order to allow better
Wilmer Ricciotti [Fri, 9 Sep 2011 13:11:36 +0000 (13:11 +0000)]
Matitaweb: layout change in the matitaweb inteface, in order to allow better
cross-browser compatibility.

13 years ago- news update
Ferruccio Guidi [Fri, 9 Sep 2011 12:21:22 +0000 (12:21 +0000)]
- news update
- the download directory is now complete

13 years ago- helm server url updated
Ferruccio Guidi [Thu, 8 Sep 2011 21:28:55 +0000 (21:28 +0000)]
- helm server url updated
- some renaming

13 years agoinitial commit of lambda_delta web site
Ferruccio Guidi [Thu, 8 Sep 2011 20:36:58 +0000 (20:36 +0000)]
initial commit of lambda_delta web site
(it was not maintained in svn so far)

13 years ago- support for transitive closures started
Ferruccio Guidi [Thu, 8 Sep 2011 19:48:13 +0000 (19:48 +0000)]
- support for transitive closures started
- "unfold" component started
- we corrected one axiom of drop

13 years agoMatitaweb: fixed "new file".
matitaweb [Thu, 8 Sep 2011 15:11:18 +0000 (15:11 +0000)]
Matitaweb: fixed "new file".

13 years agoMatitaweb: New File functionality.
Wilmer Ricciotti [Thu, 8 Sep 2011 15:07:01 +0000 (15:07 +0000)]
Matitaweb: New File functionality.

13 years agoMatitaweb: Save as...
matitaweb [Thu, 8 Sep 2011 14:44:58 +0000 (14:44 +0000)]
Matitaweb: Save as...

13 years agoMatitaweb: makefile reverted to old (working) version.
matitaweb [Thu, 8 Sep 2011 14:12:38 +0000 (14:12 +0000)]
Matitaweb: makefile reverted to old (working) version.

13 years agoMatitaweb: first attempt at "Save as".
Wilmer Ricciotti [Thu, 8 Sep 2011 14:11:12 +0000 (14:11 +0000)]
Matitaweb: first attempt at "Save as".

13 years agoMatitaweb: more changes to file selection dialog box.
matitaweb [Thu, 8 Sep 2011 13:38:36 +0000 (13:38 +0000)]
Matitaweb: more changes to file selection dialog box.

13 years agoMatitaweb: changes to file selection dialog box.
Wilmer Ricciotti [Thu, 8 Sep 2011 12:58:31 +0000 (12:58 +0000)]
Matitaweb: changes to file selection dialog box.

13 years agoMatitaweb: changes to file selection dialog box.
matitaweb [Thu, 8 Sep 2011 12:58:06 +0000 (12:58 +0000)]
Matitaweb: changes to file selection dialog box.

13 years agoMatitaweb: changes in file selection dialog box.
Wilmer Ricciotti [Thu, 8 Sep 2011 12:47:37 +0000 (12:47 +0000)]
Matitaweb: changes in file selection dialog box.

13 years agoMatitaweb: Changes to the file selection dialog box.
matitaweb [Thu, 8 Sep 2011 12:44:12 +0000 (12:44 +0000)]
Matitaweb: Changes to the file selection dialog box.

13 years agoMatitaweb: changes to file selection dialog box.
Wilmer Ricciotti [Thu, 8 Sep 2011 12:40:37 +0000 (12:40 +0000)]
Matitaweb: changes to file selection dialog box.

13 years agoMatitaweb: Some changes in file selection dialogbox.
Wilmer Ricciotti [Thu, 8 Sep 2011 12:32:18 +0000 (12:32 +0000)]
Matitaweb: Some changes in file selection dialogbox.

13 years ago...
matitaweb [Wed, 7 Sep 2011 14:04:31 +0000 (14:04 +0000)]
...

13 years agoChanged behavior in matitaweb.js, function retrieveFile (it is now
matitaweb [Wed, 7 Sep 2011 13:47:44 +0000 (13:47 +0000)]
Changed behavior in matitaweb.js, function retrieveFile (it is now
compatible with Firefox, hopefully).

13 years agologic.ma is now enriched using the correct syntax.
matitaweb [Wed, 7 Sep 2011 12:48:18 +0000 (12:48 +0000)]
logic.ma is now enriched using the correct syntax.

13 years agoChanged redirect behaviour of the daemon (incompatibility with browsers
Wilmer Ricciotti [Wed, 7 Sep 2011 12:24:46 +0000 (12:24 +0000)]
Changed redirect behaviour of the daemon (incompatibility with browsers
different from google chrome).

13 years ago- confluence of context-free reduction on terms (tpr) closed!
Ferruccio Guidi [Tue, 6 Sep 2011 16:30:41 +0000 (16:30 +0000)]
- confluence of context-free reduction on terms (tpr) closed!
- substitution lemma for tpr closed!
- so-called "substitution lemma" closed!
- some annotating

13 years agoWhen the user db is not found, matitaweb now creates a new one.
Wilmer Ricciotti [Tue, 6 Sep 2011 12:28:13 +0000 (12:28 +0000)]
When the user db is not found, matitaweb now creates a new one.

13 years agoRemoved ghost copy of a MatitaScriptLexer (moved from
matitaweb [Tue, 6 Sep 2011 12:24:51 +0000 (12:24 +0000)]
Removed ghost copy of a MatitaScriptLexer (moved from
components/content_pres/ to matita/)

13 years agoFirst attempt at svn commit of developments.
Wilmer Ricciotti [Tue, 6 Sep 2011 12:00:20 +0000 (12:00 +0000)]
First attempt at svn commit of developments.
Fixes a problem with hyperlinks (the </A> tag was not consumed correctly
if it appeared at the end of a command/tactic).

13 years ago- the substitution lemma is proved!
Ferruccio Guidi [Mon, 5 Sep 2011 13:55:42 +0000 (13:55 +0000)]
- the substitution lemma is proved!
- slight modification of parallel substitution and some renaming

13 years agocommit by user utente
Wilmer Ricciotti [Mon, 5 Sep 2011 11:48:38 +0000 (11:48 +0000)]
commit by user utente

13 years agocommit by user utente
Wilmer Ricciotti [Mon, 5 Sep 2011 11:28:56 +0000 (11:28 +0000)]
commit by user utente

13 years ago- the theory of parallel substitution of local environments (ltps) is ready
Ferruccio Guidi [Fri, 2 Sep 2011 20:23:07 +0000 (20:23 +0000)]
- the theory of parallel substitution of local environments (ltps) is ready
- the theory of context-free parallel reduction of local environments (ltpr) is ready
- the proof of the substitution lemma for context-free parallel reduction is started ...
- some renaming and annotating

13 years ago- we shared the atomic term constructions
Ferruccio Guidi [Mon, 29 Aug 2011 15:21:40 +0000 (15:21 +0000)]
- we shared the atomic term constructions
- we fixed the notation of the binary term construction
- we inverted the dependences of cl_shift and cl_weight

13 years ago- the shift function is now defined and cpr_shift_fwd is proved
Ferruccio Guidi [Sat, 27 Aug 2011 13:59:35 +0000 (13:59 +0000)]
- the shift function is now defined and cpr_shift_fwd is proved
- tentative definition of the structures for the wh normal forms
- definition of lists without the [...] notation
- some refactoring and annotating (we separate lemmas from facts)

13 years ago- weakening leq, we proved cpr_bind_dx
Ferruccio Guidi [Thu, 25 Aug 2011 13:20:47 +0000 (13:20 +0000)]
- weakening leq, we proved cpr_bind_dx
- we imple,ented some statistics in the Makefile

13 years agoone reduction rule (tpr) was redundant
Ferruccio Guidi [Wed, 24 Aug 2011 17:48:10 +0000 (17:48 +0000)]
one reduction rule (tpr) was redundant

13 years ago- confluence of parallel substitution (tps) closed! (a bug in an
Ferruccio Guidi [Tue, 23 Aug 2011 17:07:23 +0000 (17:07 +0000)]
- confluence of parallel substitution (tps) closed! (a bug in an
inversion lemma was in the way)
- some refactoring

13 years agowe now use non-telescopic substitution in parallel reduction, rather
Ferruccio Guidi [Mon, 22 Aug 2011 12:34:34 +0000 (12:34 +0000)]
we now use non-telescopic substitution in parallel reduction, rather
than the telescopic one. This choice weakens the step of
context-sensitive reduction a bit while maintaining the expected
properties

13 years ago- tentative definition of lcpr (contex-sensitive parallel reduction on
Ferruccio Guidi [Fri, 19 Aug 2011 13:57:35 +0000 (13:57 +0000)]
- tentative definition of lcpr (contex-sensitive parallel reduction on
local environments)
- some refactoring

13 years agothe refactoring was not really complete
Ferruccio Guidi [Thu, 18 Aug 2011 22:14:59 +0000 (22:14 +0000)]
the refactoring was not really complete

13 years agorefactoring completed
Ferruccio Guidi [Thu, 18 Aug 2011 22:09:54 +0000 (22:09 +0000)]
refactoring completed

13 years ago- some refactoring
Ferruccio Guidi [Thu, 18 Aug 2011 22:07:11 +0000 (22:07 +0000)]
- some refactoring
- we fixed some wrong preambles in the scripts

13 years ago- matitaclean greatly improved but ...
Ferruccio Guidi [Thu, 18 Aug 2011 20:11:59 +0000 (20:11 +0000)]
- matitaclean greatly improved but ...
...  LibraryClean.clean_baseuris is not implemented yet :D

13 years agorefactoring completed!
Ferruccio Guidi [Wed, 10 Aug 2011 15:12:59 +0000 (15:12 +0000)]
refactoring completed!

13 years agothe refactoring continues ...
Ferruccio Guidi [Wed, 10 Aug 2011 12:49:38 +0000 (12:49 +0000)]
the refactoring continues ...

13 years agothe refactoring continues ...
Ferruccio Guidi [Wed, 10 Aug 2011 12:28:45 +0000 (12:28 +0000)]
the refactoring continues ...

13 years agolambda-delta must be a contrib
Ferruccio Guidi [Wed, 10 Aug 2011 11:47:21 +0000 (11:47 +0000)]
lambda-delta must be a contrib

13 years agolambda-delta must be a contrib
Ferruccio Guidi [Wed, 10 Aug 2011 11:23:43 +0000 (11:23 +0000)]
lambda-delta must be a contrib

13 years agosome refactoring
Ferruccio Guidi [Wed, 10 Aug 2011 11:13:18 +0000 (11:13 +0000)]
some refactoring

13 years agoconfluence of parallel substitution (tps) started ...
Ferruccio Guidi [Tue, 9 Aug 2011 18:46:44 +0000 (18:46 +0000)]
confluence of parallel substitution (tps) started ...

13 years ago- tps_tpr closed! (substitution is a reduction)
Ferruccio Guidi [Mon, 8 Aug 2011 22:41:37 +0000 (22:41 +0000)]
- tps_tpr closed! (substitution is a reduction)
- some refactoring