]>
matita.cs.unibo.it Git - helm.git/log
Stefano Zacchiroli [Tue, 2 Mar 2004 17:12:58 +0000 (17:12 +0000)]
differentieted empty substitution list from no substitution given
Stefano Zacchiroli [Tue, 2 Mar 2004 17:12:19 +0000 (17:12 +0000)]
- regtest now handles more than one interpretation: the tests committed
here have been ported to latest regtest format
- more informative failure report
Stefano Zacchiroli [Tue, 2 Mar 2004 15:53:19 +0000 (15:53 +0000)]
added cast concrete syntax
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 15:19:06 +0000 (15:19 +0000)]
The regression tests now check also the generated disambiguation environments.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 14:53:13 +0000 (14:53 +0000)]
Regtest fixed. It can now work also with multiple answers.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 13:20:11 +0000 (13:20 +0000)]
The disambiguation now returns a list of interpretations.
Note: the regtest is broken by this commit.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 13:18:13 +0000 (13:18 +0000)]
The disambiguation now returns a list of interpretations.
Ferruccio Guidi [Fri, 27 Feb 2004 14:06:41 +0000 (14:06 +0000)]
now database interfaces are more abstract
Ferruccio Guidi [Thu, 26 Feb 2004 17:05:53 +0000 (17:05 +0000)]
- MySQL mode added to the interpreter
- hxp restored
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:55:44 +0000 (16:55 +0000)]
Error message fixed.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:34:25 +0000 (16:34 +0000)]
...
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:32:43 +0000 (16:32 +0000)]
triciclo.conf.xml ==> gTopLevel.conf.xml
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:29:38 +0000 (16:29 +0000)]
Added () to MQInit.init.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:18:15 +0000 (16:18 +0000)]
New implementation of eat_prods. Some residual problems disappear.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:14:58 +0000 (16:14 +0000)]
New implementation of eat_prods.
In theory we expected it to be less efficient.
In pratice it is MUCH more efficient.
The old implementation is still there, but commented out.
We have to investigate the mistery a bit more.
Stefano Zacchiroli [Thu, 26 Feb 2004 16:14:58 +0000 (16:14 +0000)]
- better handling of temp files wrt to failures. When a temp file has
been created and an exception is raised, the exception will be
catched, the tempfile deleted and the exception raised again
Stefano Zacchiroli [Thu, 26 Feb 2004 14:53:18 +0000 (14:53 +0000)]
added support for commands and scripts
Stefano Zacchiroli [Thu, 26 Feb 2004 14:52:57 +0000 (14:52 +0000)]
added vim modeline for encoding=utf8
Stefano Zacchiroli [Thu, 26 Feb 2004 14:52:16 +0000 (14:52 +0000)]
added command and script ASTs with _debugging_only_ pretty printers
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 13:19:18 +0000 (13:19 +0000)]
Bug fixed: names of just one character were not inserted into the objectName.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 12:51:01 +0000 (12:51 +0000)]
One MQInterpreter commit broke regtest.ml. Fixed.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 12:01:27 +0000 (12:01 +0000)]
Optimization: since an invariant says that the inferred type of a term is
always a type, then we do not have to call the sort_of_prod to check the
the type of a lambda-abstraction is a well-typed prod. We just have to check
that the source of the lambda is a sort (or a meta).
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 11:45:02 +0000 (11:45 +0000)]
...
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 11:42:25 +0000 (11:42 +0000)]
eqT removed.
Claudio Sacerdoti Coen [Wed, 25 Feb 2004 11:27:00 +0000 (11:27 +0000)]
Variable redefined. Fixed.
Stefano Zacchiroli [Tue, 24 Feb 2004 17:33:53 +0000 (17:33 +0000)]
added mathitaGui.mli
Stefano Zacchiroli [Tue, 24 Feb 2004 17:30:06 +0000 (17:30 +0000)]
snapshot
Stefano Zacchiroli [Tue, 24 Feb 2004 16:09:38 +0000 (16:09 +0000)]
added functions and uris for binary {positive,integer}
Stefano Zacchiroli [Tue, 24 Feb 2004 16:09:10 +0000 (16:09 +0000)]
added binary {positive,integer} notation
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 15:45:31 +0000 (15:45 +0000)]
New v8.0 URIs.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 15:39:22 +0000 (15:39 +0000)]
More uris ported to V8.0.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 15:22:16 +0000 (15:22 +0000)]
More V8.0 uris.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 15:21:40 +0000 (15:21 +0000)]
More v8.0 URIs.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 15:07:38 +0000 (15:07 +0000)]
Porting URIs to V8.0.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 14:56:24 +0000 (14:56 +0000)]
Partial porting to V8 URIs.
Almost nothing has been tested yet.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 14:55:17 +0000 (14:55 +0000)]
Porting to MySql.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 14:53:06 +0000 (14:53 +0000)]
MySQL is case sensitive.
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 14:50:11 +0000 (14:50 +0000)]
Quick patch to make everything work with MySql.
Note: to compile you need to make a symbolic link from mQIDataBase.ml
to mQIPostgres.ml or mQIMySql.ml
Stefano Zacchiroli [Tue, 24 Feb 2004 13:15:48 +0000 (13:15 +0000)]
- added support for boolean parameters
- added support for optional parameters
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 10:21:17 +0000 (10:21 +0000)]
...
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 10:15:36 +0000 (10:15 +0000)]
- Targets reorganized
- new targets
Claudio Sacerdoti Coen [Tue, 24 Feb 2004 10:05:03 +0000 (10:05 +0000)]
Added parameter format=text|xml to getalluris.
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 18:36:54 +0000 (18:36 +0000)]
A lazy value was put in place of a function ==> the memoized value was no
longer updated. Fixed.
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 18:01:11 +0000 (18:01 +0000)]
"add_server?position=0" no longer worked (raised an assertion failure)
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 17:24:51 +0000 (17:24 +0000)]
No longer in use.
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 16:29:14 +0000 (16:29 +0000)]
Script to create and drop tables and indexes committed.
New targets added to the Makefile.
Stefano Zacchiroli [Mon, 23 Feb 2004 16:04:41 +0000 (16:04 +0000)]
added a space between term and "using" keyword
Stefano Zacchiroli [Mon, 23 Feb 2004 16:04:24 +0000 (16:04 +0000)]
commented out a debugging message
Stefano Zacchiroli [Mon, 23 Feb 2004 16:02:36 +0000 (16:02 +0000)]
bugfix in "elim ... using" tactical ("using" is a keyword)
Stefano Zacchiroli [Mon, 23 Feb 2004 15:56:35 +0000 (15:56 +0000)]
added a lot of notation: arithmetic operators, relational operators, ...
Stefano Zacchiroli [Mon, 23 Feb 2004 15:56:10 +0000 (15:56 +0000)]
Rinv typo fix
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 14:11:16 +0000 (14:11 +0000)]
-memory leaks fixed
- INSERT INTO objectName .... was not quoted correctly
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 14:03:49 +0000 (14:03 +0000)]
The metadata extractor now generates also
"INSERT INTO objectName ..."
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 13:12:40 +0000 (13:12 +0000)]
New framework for metadata generation.
NOTE: from this release on the metadata are inserted into a MySQL DB.
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 12:59:35 +0000 (12:59 +0000)]
(Very)* Old stuff removed.
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 12:50:57 +0000 (12:50 +0000)]
Bug fix: the generated XML for DCs was not well-formed.
Claudio Sacerdoti Coen [Mon, 23 Feb 2004 12:42:04 +0000 (12:42 +0000)]
kind=dc implemented.
Stefano Zacchiroli [Mon, 23 Feb 2004 10:27:44 +0000 (10:27 +0000)]
support optional keys in configuration file
Stefano Zacchiroli [Mon, 23 Feb 2004 10:27:27 +0000 (10:27 +0000)]
removed password entry, now uses "helm" user (read-only access is
enough for rdfly)
Luca Padovani [Sat, 21 Feb 2004 18:51:25 +0000 (18:51 +0000)]
* update for 0.0.5
Luca Padovani [Sat, 21 Feb 2004 18:48:38 +0000 (18:48 +0000)]
* cleanup
Luca Padovani [Sat, 21 Feb 2004 18:47:50 +0000 (18:47 +0000)]
* fix so that ocamlmklib works
Luca Padovani [Sat, 21 Feb 2004 10:00:02 +0000 (10:00 +0000)]
* removed debian dir from EXTRA_DIST var
Luca Padovani [Sat, 21 Feb 2004 09:59:26 +0000 (09:59 +0000)]
* using non-diffing mathml factory
* removed methods no longer implemented in gtkmathview from interface
Luca Padovani [Sat, 21 Feb 2004 09:58:05 +0000 (09:58 +0000)]
* updated the updating method so that the root element is not changed
(removes the listeners in the new editor)
Luca Padovani [Sat, 21 Feb 2004 09:52:56 +0000 (09:52 +0000)]
* added wrapper element around processed document
Luca Padovani [Sat, 21 Feb 2004 09:52:24 +0000 (09:52 +0000)]
* fixed profiling flags
Claudio Sacerdoti Coen [Fri, 20 Feb 2004 18:25:59 +0000 (18:25 +0000)]
...
Stefano Zacchiroli [Fri, 20 Feb 2004 18:03:21 +0000 (18:03 +0000)]
first check in of mathita gui
Stefano Zacchiroli [Fri, 20 Feb 2004 18:00:54 +0000 (18:00 +0000)]
bugfix: "in" is an IDENT, not a keyword
Claudio Sacerdoti Coen [Fri, 20 Feb 2004 17:44:26 +0000 (17:44 +0000)]
Quick patch to use rdfly (URL hard-coded everywhere).
Ferruccio Guidi [Fri, 20 Feb 2004 17:12:56 +0000 (17:12 +0000)]
hard-coded timing of generated queries disabled: use T interpreter flag instead.
Claudio Sacerdoti Coen [Fri, 20 Feb 2004 16:47:21 +0000 (16:47 +0000)]
Ported to
- Helm_registry
- Mysql
Ferruccio Guidi [Fri, 20 Feb 2004 16:31:07 +0000 (16:31 +0000)]
- mathql interpreter flags reorganized
- logging function in NQIConn.init is now optional: default is ignore
Claudio Sacerdoti Coen [Fri, 20 Feb 2004 14:55:53 +0000 (14:55 +0000)]
A brand new daemon: rdfly.
Ferruccio Guidi [Thu, 19 Feb 2004 15:49:01 +0000 (15:49 +0000)]
source logging patched
Ferruccio Guidi [Thu, 19 Feb 2004 15:28:43 +0000 (15:28 +0000)]
new mathql interpreterr flag V
Ferruccio Guidi [Thu, 19 Feb 2004 15:18:52 +0000 (15:18 +0000)]
source logging is now native in the interpreter
Ferruccio Guidi [Thu, 19 Feb 2004 14:34:15 +0000 (14:34 +0000)]
source logging enabled by default
Andrea Asperti [Thu, 19 Feb 2004 08:32:56 +0000 (08:32 +0000)]
Adding tacticAst2Box (pretty printer for tactical, preliminary version).
Andrea Asperti [Thu, 19 Feb 2004 08:27:20 +0000 (08:27 +0000)]
Minor modification in test_parser (to use the new pretty printer for
tacticals).
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 18:14:58 +0000 (18:14 +0000)]
...
Ferruccio Guidi [Wed, 18 Feb 2004 17:52:54 +0000 (17:52 +0000)]
mathql interpreter flags can be now red from helm registry
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 17:13:03 +0000 (17:13 +0000)]
...
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:42:34 +0000 (16:42 +0000)]
uwobo ==> uwobo.opt
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:40:36 +0000 (16:40 +0000)]
...
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:37:31 +0000 (16:37 +0000)]
Stuff moved around.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:26:35 +0000 (16:26 +0000)]
ENVSCRIPT and mathql_db_map.txt no longer in use.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 16:11:27 +0000 (16:11 +0000)]
Removed stuff no longer in use.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 15:47:23 +0000 (15:47 +0000)]
helm_registry is already in due to transitive dependencies
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.
Claudio Sacerdoti Coen [Wed, 18 Feb 2004 15:41:06 +0000 (15:41 +0000)]
typo fixed. Used to break the ls method.
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
Stefano Zacchiroli [Wed, 18 Feb 2004 14:24:11 +0000 (14:24 +0000)]
fixed cosmetic typos during pretty printing
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)
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
Ferruccio Guidi [Wed, 18 Feb 2004 13:10:17 +0000 (13:10 +0000)]
patched
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
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).
Stefano Zacchiroli [Tue, 17 Feb 2004 23:59:07 +0000 (23:59 +0000)]
added copyright info