]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 17:51:45 +0000 (17:51 +0000)]
MutCase branches must be parsed and printed using \Rightarrow.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 17:48:50 +0000 (17:48 +0000)]
Branch of MutCase must be parsed and printed using \Rightarrow.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:43:46 +0000 (16:43 +0000)]
Debugging message removed.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:42:29 +0000 (16:42 +0000)]
apply_subst did not apply the substitution to the explicit named substitution
(local context) of a variable.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:20:42 +0000 (16:20 +0000)]
Refine now raises only RefineFailure, AssertFailure or Uncertain.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:20:29 +0000 (16:20 +0000)]
Wrong error message patched.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 15:29:20 +0000 (15:29 +0000)]
List.nth not guarded by try ... with. Fixed.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 14:20:34 +0000 (14:20 +0000)]
Debugging code removed.
Query logging is already implemented. It can be activated from the
.conf.xml file.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 14:19:42 +0000 (14:19 +0000)]
HelmLogger logging function connected to MathQL Interpreter logger function.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 12:24:05 +0000 (12:24 +0000)]
Syntax of explicit named substitions syncronized with the parser.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 23:46:42 +0000 (23:46 +0000)]
Yet another error in the id regexp: numbers are allowed in identifiers, as well
as 's.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 23:37:08 +0000 (23:37 +0000)]
Bug in guarded_by_destructors (case Rel to a definition in the context) fixed.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 18:56:53 +0000 (18:56 +0000)]
Big bug fixed: batchParser applied the varsprefix prefix also to
constants and inductive types!!!
It is now possible to specify independently the prefix for variables and
the prefix for all the other objects.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 18:30:25 +0000 (18:30 +0000)]
Improved output when [ MANY ] occurs.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 17:54:40 +0000 (17:54 +0000)]
...
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 17:39:57 +0000 (17:39 +0000)]
...
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 17:30:06 +0000 (17:30 +0000)]
- Improved error messaging.
- Invalid_argument was raised by List.fold_left2 ;-(
I want checked excecptions!
Stefano Zacchiroli [Tue, 2 Mar 2004 17:14:15 +0000 (17:14 +0000)]
- ported to latest CicAst.Ident format (Some [] <> None)
- unspecified local contexes are now inferred
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)]
...