]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agomathql interpreter flags can be now red from helm registry
Ferruccio Guidi [Wed, 18 Feb 2004 17:52:54 +0000 (17:52 +0000)]
mathql interpreter flags can be now red from helm registry

20 years ago...
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 17:13:03 +0000 (17:13 +0000)]
...

20 years agouwobo ==> uwobo.opt
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:42:34 +0000 (16:42 +0000)]
uwobo ==> uwobo.opt

20 years ago...
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:40:36 +0000 (16:40 +0000)]
...

20 years agoStuff moved around.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:37:31 +0000 (16:37 +0000)]
Stuff moved around.

20 years agoENVSCRIPT and mathql_db_map.txt no longer in use.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:26:35 +0000 (16:26 +0000)]
ENVSCRIPT and mathql_db_map.txt no longer in use.

20 years agoRemoved stuff no longer in use.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:11:27 +0000 (16:11 +0000)]
Removed stuff no longer in use.

20 years agohelm_registry is already in due to transitive dependencies
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 15:47:23 +0000 (15:47 +0000)]
helm_registry is already in due to transitive dependencies

20 years agoThe order IS significative. Changing the order (in one of the last commits)
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 15:41:35 +0000 (15:41 +0000)]
The order IS significative. Changing the order (in one of the last commits)
broke the ls method.

20 years agotypo fixed. Used to break the ls method.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 15:41:06 +0000 (15:41 +0000)]
typo fixed. Used to break the ls method.

20 years ago- better error message on "unknown identifier"
Stefano Zacchiroli [Wed, 18 Feb 2004 14:25:35 +0000 (14:25 +0000)]
- better error message on "unknown identifier"
- use newer (Andrea and Luca)'s box-based-pretty-printer

20 years agofixed cosmetic typos during pretty printing
Stefano Zacchiroli [Wed, 18 Feb 2004 14:24:11 +0000 (14:24 +0000)]
fixed cosmetic typos during pretty printing

20 years ago- bugfix in term grammar: lowered precedence level of "let ... in" so
Stefano Zacchiroli [Wed, 18 Feb 2004 14:22:49 +0000 (14:22 +0000)]
- bugfix in term grammar: lowered precedence level of "let ... in" so
  that "let x = 1 in x + 2" works as expected
- decent grammar for tactics and tacticals: now with precedence levels
  (no more stackoverflows, hopefully)

20 years agocatch parse error exception and show them to the user during main loop
Stefano Zacchiroli [Wed, 18 Feb 2004 14:21:27 +0000 (14:21 +0000)]
catch parse error exception and show them to the user during main loop

20 years agopatched
Ferruccio Guidi [Wed, 18 Feb 2004 13:10:17 +0000 (13:10 +0000)]
patched

20 years agobatchParser and regtest patched to avoid a non encapsulated connection to the mathql...
Ferruccio Guidi [Wed, 18 Feb 2004 11:33:13 +0000 (11:33 +0000)]
batchParser and regtest patched to avoid a non encapsulated connection to the mathql interpreter

20 years agoBug fixed: Helm_registry was used not enough lazily (i.e. before loading
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 10:00:15 +0000 (10:00 +0000)]
Bug fixed: Helm_registry was used not enough lazily (i.e. before loading
the configuration).

20 years agoadded copyright info
Stefano Zacchiroli [Tue, 17 Feb 2004 23:59:07 +0000 (23:59 +0000)]
added copyright info

20 years agoremoved useless Mpresentation module
Stefano Zacchiroli [Tue, 17 Feb 2004 23:58:30 +0000 (23:58 +0000)]
removed useless Mpresentation module

20 years agomoved away tactics and tacticals
Stefano Zacchiroli [Tue, 17 Feb 2004 23:58:08 +0000 (23:58 +0000)]
moved away tactics and tacticals

20 years agoadded tactics and tacticals (heavily bugged)
Stefano Zacchiroli [Tue, 17 Feb 2004 23:57:44 +0000 (23:57 +0000)]
added tactics and tacticals (heavily bugged)

20 years agoadded hook for .cma link time options
Stefano Zacchiroli [Tue, 17 Feb 2004 23:56:54 +0000 (23:56 +0000)]
added hook for .cma link time options

20 years agoadded tactic and tactical (still heavily bugged!!!)
Stefano Zacchiroli [Tue, 17 Feb 2004 23:56:28 +0000 (23:56 +0000)]
added tactic and tactical (still heavily bugged!!!)

20 years ago68080 (that overflows ; -) ==> 38080
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 18:13:20 +0000 (18:13 +0000)]
68080 (that overflows ; -) ==> 38080

20 years agofixed typo
Stefano Zacchiroli [Tue, 17 Feb 2004 18:12:38 +0000 (18:12 +0000)]
fixed typo

20 years agoNew key postgresql_connection_string.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 18:11:57 +0000 (18:11 +0000)]
New key postgresql_connection_string.

20 years agoremoved (now useless) connection string line
Stefano Zacchiroli [Tue, 17 Feb 2004 18:10:58 +0000 (18:10 +0000)]
removed (now useless) connection string line

20 years agoNew key mathql_interpreter.postgresql_connection_string.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 18:02:55 +0000 (18:02 +0000)]
New key mathql_interpreter.postgresql_connection_string.

20 years agoThe PostgreSQL connection string has been moved to the Helm_registry
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:58:42 +0000 (17:58 +0000)]
The PostgreSQL connection string has been moved to the Helm_registry
(key mathql_interpreter.postgresql_connection_string).

20 years agoOther stuff no longer used removed.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:50:40 +0000 (17:50 +0000)]
Other stuff no longer used removed.

20 years agoSeveral no longer used variables removed.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:49:06 +0000 (17:49 +0000)]
Several no longer used variables removed.

20 years agoPorting of applyStylesheets.ml to Helm_registry.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:41:33 +0000 (17:41 +0000)]
Porting of applyStylesheets.ml to Helm_registry.

20 years agoReindentation.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:38:22 +0000 (17:38 +0000)]
Reindentation.

20 years agomathql_db_map.txt now retrieved by Helm_registry.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:23:58 +0000 (17:23 +0000)]
mathql_db_map.txt now retrieved by Helm_registry.

20 years agomathql_db_map.txt is now retrieved by Helm_registry.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 17:20:57 +0000 (17:20 +0000)]
mathql_db_map.txt is now retrieved by Helm_registry.

20 years ago-linkall removed
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 16:59:34 +0000 (16:59 +0000)]
-linkall removed

20 years ago- ported to Helm_registry
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 16:33:19 +0000 (16:33 +0000)]
- ported to Helm_registry
- ported to the new disambiguating parser of Zack & Andrea

20 years agosearchEngine ported to Helm_registry.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 14:52:14 +0000 (14:52 +0000)]
searchEngine ported to Helm_registry.

20 years agofixed typo
Stefano Zacchiroli [Tue, 17 Feb 2004 12:47:21 +0000 (12:47 +0000)]
fixed typo

20 years agoAll daemons are now run in their .opt version.
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 11:41:55 +0000 (11:41 +0000)]
All daemons are now run in their .opt version.

20 years agoAny residual reference to tomcat and servlets changed to references to
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 11:40:05 +0000 (11:40 +0000)]
Any residual reference to tomcat and servlets changed to references to
Web-Services ;-)

20 years ago- double_type_of: sort_of_prod modified to expect also a meta
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 10:48:11 +0000 (10:48 +0000)]
- double_type_of: sort_of_prod modified to expect also a meta
- cic2acic: string_of_sort badly patched to return a "?" when a meta
  is found. Note: this solution is not admissible, since it generates
  non-valid XML files (and it may also break other things).

20 years agotriciclo.conf.xml ==> gTopLevel.conf.xml
Claudio Sacerdoti Coen [Tue, 17 Feb 2004 10:47:02 +0000 (10:47 +0000)]
triciclo.conf.xml ==> gTopLevel.conf.xml

20 years agoMore daemons ported to Helm_registry.
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 22:59:57 +0000 (22:59 +0000)]
More daemons ported to Helm_registry.

20 years agodrawGraph ported to Helm_registry.
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 22:59:21 +0000 (22:59 +0000)]
drawGraph ported to Helm_registry.

20 years agoPorting of uriSetQueue to Helm_registry.
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 22:50:06 +0000 (22:50 +0000)]
Porting of uriSetQueue to Helm_registry.

20 years agoproofChecker ported to Helm_registry
Claudio Sacerdoti Coen [Mon, 16 Feb 2004 22:11:57 +0000 (22:11 +0000)]
proofChecker ported to Helm_registry

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).