]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years ago- Ported to latest version of Helm_registry
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 22:09:01 +0000 (22:09 +0000)]
- Ported to latest version of Helm_registry

20 years ago- Uwobo ported to Helm_registry
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 21:42:29 +0000 (21:42 +0000)]
- Uwobo ported to Helm_registry
- Environment variables used only by loadPredefinedStylesheets.pl moved from
  template.* to etc_default_helm_mowgli

20 years agoCached moved to /tmp/helm/cache.
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 18:28:50 +0000 (18:28 +0000)]
Cached moved to /tmp/helm/cache.

20 years agoPorted to Helm_registry.
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 18:16:58 +0000 (18:16 +0000)]
Ported to Helm_registry.

20 years ago...
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 17:26:38 +0000 (17:26 +0000)]
...

20 years ago...
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 17:24:44 +0000 (17:24 +0000)]
...

20 years agobugfix: top level keys now should work
Stefano Zacchiroli [Mon, 16 Feb 2004 17:24:14 +0000 (17:24 +0000)]
bugfix: top level keys now should work

20 years ago- Configuration file moved to /projects/helm/etc.
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 17:21:30 +0000 (17:21 +0000)]
- Configuration file moved to /projects/helm/etc.
- Configuration file ported to latest version of Helm_registry.

20 years ago- triciclo.conf.xml.sample ported to the latest version of Helm_registry
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 17:09:47 +0000 (17:09 +0000)]
- triciclo.conf.xml.sample ported to the latest version of Helm_registry
- annotations.{url,dir} renamed into local_library.{url,dir}

20 years ago- more structured configuration file
Stefano Zacchiroli [Mon, 16 Feb 2004 16:43:27 +0000 (16:43 +0000)]
- more structured configuration file
- commented out save_to since it's not yet implemented for the new XML format

20 years agotypo fixed (unbalanced parens)
Stefano Zacchiroli [Mon, 16 Feb 2004 10:13:47 +0000 (10:13 +0000)]
typo fixed (unbalanced parens)

20 years agoadded ocamlinit target which creates a .ocamlinit file
Stefano Zacchiroli [Mon, 16 Feb 2004 09:48:18 +0000 (09:48 +0000)]
added ocamlinit target which creates a .ocamlinit file

20 years agosolved a precedence issue between binders and arrows
Stefano Zacchiroli [Mon, 16 Feb 2004 09:44:14 +0000 (09:44 +0000)]
solved a precedence issue between binders and arrows

20 years agodo not use tex notation per default (used only by tex term editor)
Stefano Zacchiroli [Mon, 16 Feb 2004 09:43:55 +0000 (09:43 +0000)]
do not use tex notation per default (used only by tex term editor)

20 years agouse BoxPp
Stefano Zacchiroli [Mon, 16 Feb 2004 09:43:25 +0000 (09:43 +0000)]
use BoxPp

20 years ago- added arrow notation
Stefano Zacchiroli [Mon, 16 Feb 2004 09:42:44 +0000 (09:42 +0000)]
- added arrow notation
- typo fixed ("Pi" vs "pi")

20 years agopatched
Ferruccio Guidi [Fri, 13 Feb 2004 15:39:53 +0000 (15:39 +0000)]
patched

20 years agoinductive type ident optional in mutcase
Stefano Zacchiroli [Fri, 13 Feb 2004 13:33:00 +0000 (13:33 +0000)]
inductive type ident optional in mutcase

20 years agoadded regtest for optional inductive type on mutcase
Stefano Zacchiroli [Fri, 13 Feb 2004 13:32:12 +0000 (13:32 +0000)]
added regtest for optional inductive type on mutcase

20 years agos/pcre/str/
Stefano Zacchiroli [Fri, 13 Feb 2004 13:21:38 +0000 (13:21 +0000)]
s/pcre/str/

20 years agonew (box based) pretty printer
Andrea Asperti [Fri, 13 Feb 2004 12:57:01 +0000 (12:57 +0000)]
new (box based) pretty printer

20 years agosplit configure.ac in two parts: ocaml and gTopLevel
Stefano Zacchiroli [Fri, 13 Feb 2004 12:29:10 +0000 (12:29 +0000)]
split configure.ac in two parts: ocaml and gTopLevel

20 years agoadded sample configuration file
Stefano Zacchiroli [Fri, 13 Feb 2004 10:08:58 +0000 (10:08 +0000)]
added sample configuration file

20 years ago- added support for variable interpolation
Stefano Zacchiroli [Fri, 13 Feb 2004 10:07:15 +0000 (10:07 +0000)]
- added support for variable interpolation
- switched from Pcre to Str for regexps :-(

20 years agopatched for *.cmx
Ferruccio Guidi [Thu, 12 Feb 2004 22:07:05 +0000 (22:07 +0000)]
patched for *.cmx

20 years agonew .depend files
Ferruccio Guidi [Thu, 12 Feb 2004 22:01:43 +0000 (22:01 +0000)]
new .depend files

20 years agoremoved some anciente debugging messages
Stefano Zacchiroli [Thu, 12 Feb 2004 12:57:39 +0000 (12:57 +0000)]
removed some anciente debugging messages

20 years agolibraries-complete.ps:
Claudio Sacerdoti Coen [Thu, 12 Feb 2004 12:22:25 +0000 (12:22 +0000)]
libraries-complete.ps:
 * square nodes now have a yellow blackground
 * pxp-* packages collapsed to a single node pxp[-*]

20 years agolibraries-complete.ps: the internal libraries are now all squares while
Claudio Sacerdoti Coen [Thu, 12 Feb 2004 12:12:46 +0000 (12:12 +0000)]
libraries-complete.ps: the internal libraries are now all squares while
the external libraries are circles.

20 years agoAdded new target libraries-complete.ps (with also all the external
Claudio Sacerdoti Coen [Thu, 12 Feb 2004 11:48:33 +0000 (11:48 +0000)]
Added new target libraries-complete.ps (with also all the external
dependencies).

20 years agoExample configuration committed.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 17:54:45 +0000 (17:54 +0000)]
Example configuration committed.

20 years agoPorted to Http_registry and to HelmLogger.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 17:51:45 +0000 (17:51 +0000)]
Ported to Http_registry and to HelmLogger.

20 years agogetter's revolution (now uses backend in ocaml/getter)
Stefano Zacchiroli [Wed, 11 Feb 2004 17:17:26 +0000 (17:17 +0000)]
getter's revolution (now uses backend in ocaml/getter)

20 years agoPorted to Helm_registry.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 17:05:27 +0000 (17:05 +0000)]
Ported to Helm_registry.

20 years agobugfix: auto_disambiguation is not considered for searchPatternApply
Stefano Zacchiroli [Wed, 11 Feb 2004 16:02:18 +0000 (16:02 +0000)]
bugfix: auto_disambiguation is not considered for searchPatternApply

20 years ago- script.sh removed from CVS. script.sh.sample added isntead
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 12:17:35 +0000 (12:17 +0000)]
- script.sh removed from CVS. script.sh.sample added isntead
- triciclo.conf.xml.sample added

20 years agofixed typo
Stefano Zacchiroli [Wed, 11 Feb 2004 12:09:30 +0000 (12:09 +0000)]
fixed typo

20 years agonew logger
Stefano Zacchiroli [Wed, 11 Feb 2004 12:04:16 +0000 (12:04 +0000)]
new logger

20 years agonew getter, logger, and the hell
Stefano Zacchiroli [Wed, 11 Feb 2004 12:03:40 +0000 (12:03 +0000)]
new getter, logger, and the hell

20 years agonew logger, getter, and the hell
Stefano Zacchiroli [Wed, 11 Feb 2004 12:03:07 +0000 (12:03 +0000)]
new logger, getter, and the hell

20 years agosupport for subst
Stefano Zacchiroli [Wed, 11 Feb 2004 12:02:46 +0000 (12:02 +0000)]
support for subst

20 years agonew metas (getter's backend, registry, logger, and the hell)
Stefano Zacchiroli [Wed, 11 Feb 2004 12:02:23 +0000 (12:02 +0000)]
new metas (getter's backend, registry, logger, and the hell)

20 years agoported to new getter (backend)
Stefano Zacchiroli [Wed, 11 Feb 2004 12:01:56 +0000 (12:01 +0000)]
ported to new getter (backend)

20 years agoported to helm registry
Stefano Zacchiroli [Wed, 11 Feb 2004 12:01:08 +0000 (12:01 +0000)]
ported to helm registry

20 years agoported to new logger
Stefano Zacchiroli [Wed, 11 Feb 2004 12:00:51 +0000 (12:00 +0000)]
ported to new logger

20 years agouse debug_print in a debugging message
Stefano Zacchiroli [Wed, 11 Feb 2004 11:57:37 +0000 (11:57 +0000)]
use debug_print in a debugging message

20 years ago- getter revolution: split backend and frontend (this is the backend)
Stefano Zacchiroli [Wed, 11 Feb 2004 11:57:00 +0000 (11:57 +0000)]
- getter revolution: split backend and frontend (this is the backend)
- working remote part but not yet the local one (extra unneeded headers)

20 years ago- split away gtk logger
Stefano Zacchiroli [Wed, 11 Feb 2004 11:56:15 +0000 (11:56 +0000)]
- split away gtk logger
- renamed module to HelmLogger

20 years agoadded some debugging messages
Stefano Zacchiroli [Wed, 11 Feb 2004 11:55:42 +0000 (11:55 +0000)]
added some debugging messages

20 years agoA type checking error report now prints also the metasenv.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 11:23:05 +0000 (11:23 +0000)]
A type checking error report now prints also the metasenv.

20 years agoadded target *.opt (e.g. test.opt, librarytest.opt, etc.)
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 11:14:18 +0000 (11:14 +0000)]
added target *.opt (e.g. test.opt, librarytest.opt, etc.)

20 years ago- make *opt fixed
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 11:11:49 +0000 (11:11 +0000)]
- make *opt fixed
- added -vars -varsprefix cic:/Coq to testlibrary

20 years agoBig changes:
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 10:35:52 +0000 (10:35 +0000)]
Big changes:
  1. every level now catches the *Failure excecptions of the lower level
     and converts it to its own *Failure. The same for *Uncertain.
  2. CicMetaSubst.delift now raises also Uncertain (that is converted
     to CicUnification.Uncertain and then to CicRefine.Uncertain).

20 years agoAdded copyright notice.
Claudio Sacerdoti Coen [Wed, 11 Feb 2004 10:33:22 +0000 (10:33 +0000)]
Added copyright notice.

20 years agoExplicit Named Substitutions now supported.
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 15:25:49 +0000 (15:25 +0000)]
Explicit Named Substitutions now supported.

20 years agoCicCache ==> CicEnvironment (in testlibrary.ml)
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 14:07:21 +0000 (14:07 +0000)]
CicCache ==> CicEnvironment (in testlibrary.ml)

20 years ago- fixed final log reporting (that was broken by one of the previous commits)
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 14:06:51 +0000 (14:06 +0000)]
- fixed final log reporting (that was broken by one of the previous commits)
- CicCache ==> CicEnvironment

20 years agoBug fixed: when an axiom was asked, an exception was raised (since the
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 14:03:33 +0000 (14:03 +0000)]
Bug fixed: when an axiom was asked, an exception was raised (since the
check for an existent body was skipped).

20 years agopatched
Ferruccio Guidi [Tue, 10 Feb 2004 13:03:23 +0000 (13:03 +0000)]
patched

20 years agoOnly applications whose head was a constant were eta-fixed.
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 12:11:36 +0000 (12:11 +0000)]
Only applications whose head was a constant were eta-fixed.
Result: sometimes the generated term was no longer well-typed.
The fix consists in calling the type-checker on the head of the
applications. Slower, but more reliable.

20 years agoBug fixed: checking inductive type declarations with left parameters (e.g.
Claudio Sacerdoti Coen [Tue, 10 Feb 2004 12:07:08 +0000 (12:07 +0000)]
Bug fixed: checking inductive type declarations with left parameters (e.g.
le) lead to mistakes due to debrujin/undebrujin: terms to be debrujined must
be closed and then left parameters can not be removed _before_ calling
debrujin_constructor.

20 years agoadded "'" as a valid (continuation) identifier character
Stefano Zacchiroli [Tue, 10 Feb 2004 09:04:35 +0000 (09:04 +0000)]
added "'" as a valid (continuation) identifier character

20 years agoAdded flag ?eta_fix:bool to acic_object_of_cic_object.
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 18:43:38 +0000 (18:43 +0000)]
Added flag ?eta_fix:bool to acic_object_of_cic_object.

20 years agoadded thread entry
Stefano Zacchiroli [Mon, 9 Feb 2004 17:05:59 +0000 (17:05 +0000)]
added thread entry

20 years agoadded netstring and pxp deps
Stefano Zacchiroli [Mon, 9 Feb 2004 17:05:44 +0000 (17:05 +0000)]
added netstring and pxp deps

20 years agohelm-thread's META
Stefano Zacchiroli [Mon, 9 Feb 2004 17:05:16 +0000 (17:05 +0000)]
helm-thread's META

20 years agothread library (actually contains just ThreadSafe module)
Stefano Zacchiroli [Mon, 9 Feb 2004 17:04:36 +0000 (17:04 +0000)]
thread library (actually contains just ThreadSafe module)

20 years ago- added environment variable overriding
Stefano Zacchiroli [Mon, 9 Feb 2004 17:03:56 +0000 (17:03 +0000)]
- added environment variable overriding
- XML syntax for configuration file

20 years agosort_of_prod now thinks that a "sort metavariable" is a metavariable where
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 16:40:29 +0000 (16:40 +0000)]
sort_of_prod now thinks that a "sort metavariable" is a metavariable where
no free variable occurs in the local context. Reason: there used to be a bug
induced by the fact that a metavariable ?1 with an empty canonical context
could be istantiated with a metavariable ?2[l] where l has no free variables
but still it is not of length 0.

20 years agoAdded is_closed.
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 16:37:16 +0000 (16:37 +0000)]
Added is_closed.

20 years agosplit into two major parts:
Stefano Zacchiroli [Mon, 9 Feb 2004 13:22:00 +0000 (13:22 +0000)]
split into two major parts:
- backend (ocaml API)
- frontend (web service)

20 years agobumped version (tag soon)
Stefano Zacchiroli [Mon, 9 Feb 2004 13:18:48 +0000 (13:18 +0000)]
bumped version (tag soon)

20 years agono longer use marshalled table for unicode macros
Stefano Zacchiroli [Mon, 9 Feb 2004 09:42:15 +0000 (09:42 +0000)]
no longer use marshalled table for unicode macros

20 years agouse CicAstPp
Stefano Zacchiroli [Mon, 9 Feb 2004 09:42:02 +0000 (09:42 +0000)]
use CicAstPp

20 years agoeat_prods now uses mk_implicit_type.
Claudio Sacerdoti Coen [Mon, 9 Feb 2004 09:27:25 +0000 (09:27 +0000)]
eat_prods now uses mk_implicit_type.

20 years ago- Added mk_implicit_sort.
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 18:03:36 +0000 (18:03 +0000)]
- Added mk_implicit_sort.
- Used in CicRefine.sort_of_prod.

20 years agoAdded mk_implicit_sort.
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 18:01:53 +0000 (18:01 +0000)]
Added mk_implicit_sort.

20 years agoA better (but yet not empty) metasenv is now returned.
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 17:58:39 +0000 (17:58 +0000)]
A better (but yet not empty) metasenv is now returned.

20 years agosort_of_prod: the second term, when it is a meta, was unified with a fresh
Claudio Sacerdoti Coen [Sat, 7 Feb 2004 17:52:01 +0000 (17:52 +0000)]
sort_of_prod: the second term, when it is a meta, was unified with a fresh
meta in a wrong context. Fixed.

20 years ago- added options "-vars" and "-varsprefix"
Stefano Zacchiroli [Sat, 7 Feb 2004 10:33:09 +0000 (10:33 +0000)]
- added options "-vars" and "-varsprefix"
- ported testlibrary to Arg module

20 years agochanged deps since testlibrary now uses (minimally) BatchParser
Stefano Zacchiroli [Sat, 7 Feb 2004 10:32:38 +0000 (10:32 +0000)]
changed deps since testlibrary now uses (minimally) BatchParser

20 years agorebuilt
Stefano Zacchiroli [Sat, 7 Feb 2004 10:32:16 +0000 (10:32 +0000)]
rebuilt

20 years agosort metavariables are now generated in an empty canonical context.
Claudio Sacerdoti Coen [Fri, 6 Feb 2004 18:06:28 +0000 (18:06 +0000)]
sort metavariables are now generated in an empty canonical context.

20 years agoadded annotations to Cic.Implicit
Stefano Zacchiroli [Fri, 6 Feb 2004 17:16:20 +0000 (17:16 +0000)]
added annotations to Cic.Implicit

20 years agouse ledit for debugging
Stefano Zacchiroli [Fri, 6 Feb 2004 17:11:59 +0000 (17:11 +0000)]
use ledit for debugging

20 years agoComments (notes) removed.
Claudio Sacerdoti Coen [Fri, 6 Feb 2004 14:34:20 +0000 (14:34 +0000)]
Comments (notes) removed.

20 years agoCode riorganization.
Claudio Sacerdoti Coen [Fri, 6 Feb 2004 14:27:47 +0000 (14:27 +0000)]
Code riorganization.

20 years agoadded Format-library-friendly pretty printers defined on top of the
Stefano Zacchiroli [Fri, 6 Feb 2004 12:31:27 +0000 (12:31 +0000)]
added Format-library-friendly pretty printers defined on top of the
previous ones (still exported)

20 years agoadded -g flag to ocamlc per default
Stefano Zacchiroli [Fri, 6 Feb 2004 12:29:30 +0000 (12:29 +0000)]
added -g flag to ocamlc per default

20 years agotextual term editor is now the default one
Stefano Zacchiroli [Fri, 6 Feb 2004 12:28:58 +0000 (12:28 +0000)]
textual term editor is now the default one

20 years agoignore .debug_script (used by Makefile's debug target)
Stefano Zacchiroli [Fri, 6 Feb 2004 12:25:11 +0000 (12:25 +0000)]
ignore .debug_script (used by Makefile's debug target)

20 years ago- split regtest/testlibrary/gTopLevel objects so that the first two
Stefano Zacchiroli [Fri, 6 Feb 2004 12:24:38 +0000 (12:24 +0000)]
- split regtest/testlibrary/gTopLevel objects so that the first two
  aren't linked in thread mode
- added debug target to debug with wowcamldebug executables
- link with -g per default in bytecode mode

20 years agoBug MutCase fixed: now the type of the constructor only eats the
Andrea Asperti [Fri, 6 Feb 2004 10:25:04 +0000 (10:25 +0000)]
Bug MutCase fixed: now the type of the constructor only eats the
left params.

20 years agoadded testlibrary.opt and some cm****
Stefano Zacchiroli [Fri, 6 Feb 2004 09:19:49 +0000 (09:19 +0000)]
added testlibrary.opt and some cm****

20 years agoNameExpected exception removed. The "identifier" __n is now returned
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:30:57 +0000 (18:30 +0000)]
NameExpected exception removed. The "identifier" __n is now returned
(as CicPp does).

20 years agoImproved error messages.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:21:36 +0000 (18:21 +0000)]
Improved error messages.

20 years agoNo more garbage in the metasenv.
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:18:52 +0000 (18:18 +0000)]
No more garbage in the metasenv.

20 years agoNew target librarytest (to apply testlibrary.opt to index.txt). The output
Claudio Sacerdoti Coen [Thu, 5 Feb 2004 18:15:45 +0000 (18:15 +0000)]
New target librarytest (to apply testlibrary.opt to index.txt). The output
is in LOG.

20 years ago- added support for multiple choices
Stefano Zacchiroli [Thu, 5 Feb 2004 17:59:39 +0000 (17:59 +0000)]
- added support for multiple choices
- added pping of toplevel exceptions

20 years agobetter output format
Stefano Zacchiroli [Thu, 5 Feb 2004 17:47:07 +0000 (17:47 +0000)]
better output format