]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years ago- logging of long-running actions (like update) is now sent to the
Stefano Zacchiroli [Fri, 2 Apr 2004 11:51:04 +0000 (11:51 +0000)]
- logging of long-running actions (like update) is now sent to the
  client incrementally
- moved some frontend related functions (like return_html*) from
  Http_getter_common to the frontend (main.ml)

20 years agoremoved no longer needed password from connection string
Stefano Zacchiroli [Thu, 1 Apr 2004 17:06:27 +0000 (17:06 +0000)]
removed no longer needed password from connection string

20 years ago- added "Host:" line to http requests so that virtual hosting hosts are
Stefano Zacchiroli [Thu, 1 Apr 2004 16:59:09 +0000 (16:59 +0000)]
- added "Host:" line to http requests so that virtual hosting hosts are
  supported (and ancient HTTP are no longer supported)

20 years ago- removed http_get/http_get_iter implementations, use the analogous
Stefano Zacchiroli [Thu, 1 Apr 2004 16:58:00 +0000 (16:58 +0000)]
- removed http_get/http_get_iter implementations, use the analogous
  functions from ocaml-http

20 years ago<VARIABLE as="LocalFact"/> added
Claudio Sacerdoti Coen [Thu, 1 Apr 2004 16:40:46 +0000 (16:40 +0000)]
<VARIABLE as="LocalFact"/> added

20 years agoremoved an out of date comment
Stefano Zacchiroli [Thu, 1 Apr 2004 15:45:08 +0000 (15:45 +0000)]
removed an out of date comment

20 years agoadded hyperlinks to help message
Stefano Zacchiroli [Thu, 1 Apr 2004 15:44:50 +0000 (15:44 +0000)]
added hyperlinks to help message

20 years agoremoved out of date configuration file
Stefano Zacchiroli [Thu, 1 Apr 2004 10:14:46 +0000 (10:14 +0000)]
removed out of date configuration file

20 years agotacticChaser modified to avoid double "apply" and to avoid to apply uris ".var" in...
Matteo Selmi [Wed, 31 Mar 2004 20:21:56 +0000 (20:21 +0000)]
tacticChaser modified to avoid double "apply" and to avoid to apply uris ".var" in tactic "auto".

20 years agoMeta files are in METAS subdir
Lionel Mamane [Wed, 31 Mar 2004 14:54:52 +0000 (14:54 +0000)]
Meta files are in METAS subdir
source of meta files are called meta., not META.

20 years agoInstall to findlib-defined dest dir, not to stdlib dir
Lionel Mamane [Wed, 31 Mar 2004 11:51:56 +0000 (11:51 +0000)]
Install to findlib-defined dest dir, not to stdlib dir

20 years ago- provastruct.theory.xml removed (what was that exactly?)
Claudio Sacerdoti Coen [Tue, 30 Mar 2004 16:36:09 +0000 (16:36 +0000)]
- provastruct.theory.xml removed (what was that exactly?)
- @name of SECTION renamed to @uri

20 years agoupdating and structuring
Ferruccio Guidi [Sun, 28 Mar 2004 11:06:45 +0000 (11:06 +0000)]
updating and structuring

20 years agoAlgebra => CoRN
Claudio Sacerdoti Coen [Fri, 26 Mar 2004 14:58:17 +0000 (14:58 +0000)]
Algebra => CoRN

20 years agotex notation enabled
Claudio Sacerdoti Coen [Fri, 26 Mar 2004 14:55:16 +0000 (14:55 +0000)]
tex notation enabled

20 years ago* the .o files to be used in the dll are now taken from the .libs subdirectoy
Luca Padovani [Thu, 25 Mar 2004 11:40:41 +0000 (11:40 +0000)]
* the .o files to be used in the dll are now taken from the .libs subdirectoy
  (which presumably contains the PIC code)

20 years agoCSC: hack to make applications of constants that have a Type sort which
Stefano Zacchiroli [Wed, 24 Mar 2004 16:52:15 +0000 (16:52 +0000)]
CSC: hack to make applications of constants that have a Type sort which
occurs in contravariant position work. The idea is to generate in place
of a metavariable of type Type (that should be of type <Type) a
metavariable of type "a metavariable of type Type". The problem is that
in this way the metavariable can also be instantiated that is not a
sort.

20 years ago* added embedding test (HTML)
Luca Padovani [Wed, 24 Mar 2004 08:19:28 +0000 (08:19 +0000)]
* added embedding test (HTML)
* new things to do

20 years ago* added TODO file
Luca Padovani [Wed, 24 Mar 2004 06:35:40 +0000 (06:35 +0000)]
* added TODO file

20 years ago* added test with MathML really embedded within HTML
Luca Padovani [Tue, 23 Mar 2004 21:03:55 +0000 (21:03 +0000)]
* added test with MathML really embedded within HTML
* set plugin border to 0 (? black line still visible)
* is set SHADOW_NONE the plugin window gets dirty!!! :-(

20 years ago* implemented click so that the browser is notified with the new URL
Luca Padovani [Tue, 23 Mar 2004 14:49:46 +0000 (14:49 +0000)]
* implemented click so that the browser is notified with the new URL
  and loads it

20 years agocosmetic alignment change
Stefano Zacchiroli [Mon, 22 Mar 2004 17:48:49 +0000 (17:48 +0000)]
cosmetic alignment change

20 years ago- implemented real thread killing (in place of the previous fake implementation)
Stefano Zacchiroli [Mon, 22 Mar 2004 17:47:13 +0000 (17:47 +0000)]
- implemented real thread killing (in place of the previous fake implementation)

20 years agoload_document(_,NULL) => unload
Claudio Sacerdoti Coen [Mon, 22 Mar 2004 17:46:00 +0000 (17:46 +0000)]
load_document(_,NULL) => unload

20 years ago- power notation
Claudio Sacerdoti Coen [Mon, 22 Mar 2004 11:27:32 +0000 (11:27 +0000)]
- power notation
- mult for BinInt

*** DANGEROUS ***
- multiple NUM instances now are different instances

20 years ago...
Claudio Sacerdoti Coen [Mon, 22 Mar 2004 11:22:03 +0000 (11:22 +0000)]
...

20 years agointroduction updated
Ferruccio Guidi [Sun, 21 Mar 2004 19:31:26 +0000 (19:31 +0000)]
introduction updated

20 years agoThe operational semantics of the core language is ready
Ferruccio Guidi [Sun, 21 Mar 2004 11:15:28 +0000 (11:15 +0000)]
The operational semantics of the core language is ready

20 years agoBug fixed for theorems whose statement are like
Claudio Sacerdoti Coen [Wed, 17 Mar 2004 13:39:23 +0000 (13:39 +0000)]
Bug fixed for theorems whose statement are like

((A -> B) -> C) -> D

20 years agoSorts are no longer all convertible. To be completed once that universes are
Andrea Asperti [Tue, 16 Mar 2004 17:50:08 +0000 (17:50 +0000)]
Sorts are no longer all convertible. To be completed once that universes are
implemented.

20 years agoSorts are no longer all convertible. To be completed once that universes
Andrea Asperti [Tue, 16 Mar 2004 17:47:06 +0000 (17:47 +0000)]
Sorts are no longer all convertible. To be completed once that universes
are implemented.

20 years agoThis fails.
Andrea Asperti [Mon, 15 Mar 2004 12:36:40 +0000 (12:36 +0000)]
This fails.

20 years agoadded final version of the paper (for the records)
Stefano Zacchiroli [Sun, 14 Mar 2004 10:21:12 +0000 (10:21 +0000)]
added final version of the paper (for the records)

20 years agotalk committed
Stefano Zacchiroli [Sun, 14 Mar 2004 10:20:11 +0000 (10:20 +0000)]
talk committed

20 years agoupdating
Ferruccio Guidi [Fri, 12 Mar 2004 23:02:32 +0000 (23:02 +0000)]
updating

20 years agoNew tactic Auto.
acerioni [Fri, 12 Mar 2004 10:12:25 +0000 (10:12 +0000)]
New tactic Auto.

20 years agoFirst implementation of the Auto tactic.
acerioni [Fri, 12 Mar 2004 09:54:38 +0000 (09:54 +0000)]
First implementation of the Auto tactic.
- tacticChaser: added a function to locate all the theorem tha can be applied
- variousTactics: the Auto tactic

20 years agoType of exception changed: from exn to string.
acerioni [Fri, 12 Mar 2004 09:40:58 +0000 (09:40 +0000)]
Type of exception changed: from exn to string.

20 years ago- interpreter: the queries are printed before execution
Ferruccio Guidi [Wed, 10 Mar 2004 17:44:27 +0000 (17:44 +0000)]
- interpreter: the queries are printed before execution
- generator  : a bug in the generation of isfalse clauses was fixed

20 years agointerpretation_choices not declared
Claudio Sacerdoti Coen [Wed, 10 Mar 2004 13:11:19 +0000 (13:11 +0000)]
interpretation_choices not declared

20 years agoescape/unescape no longer works with '+';
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 16:29:49 +0000 (16:29 +0000)]
escape/unescape no longer works with '+';
replaced with encodeURIComponent and decodeURIComponent

20 years agoParameter forgot.
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 16:19:01 +0000 (16:19 +0000)]
Parameter forgot.

20 years agoPartially ported to new disambiguating parser.
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 16:09:13 +0000 (16:09 +0000)]
Partially ported to new disambiguating parser.
Some bugs left (e.g. in aliases)

20 years agoDebug code removed.
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 15:59:56 +0000 (15:59 +0000)]
Debug code removed.

20 years agoDead code removed.
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 14:59:18 +0000 (14:59 +0000)]
Dead code removed.

20 years ago- non empty metasenv after the parsing phase are now accepted
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 10:43:54 +0000 (10:43 +0000)]
- non empty metasenv after the parsing phase are now accepted
- still many bugs open (due to the new aliases for symbols)

20 years agoBug fixed: instead of generating "not ()", I generate "true" (for PostGresql)
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 10:34:31 +0000 (10:34 +0000)]
Bug fixed: instead of generating "not ()", I generate "true" (for PostGresql)
and "1" for Mysql.

20 years agoMeta no longer raise a failure. Instead they return an empty set of
Claudio Sacerdoti Coen [Tue, 9 Mar 2004 09:52:33 +0000 (09:52 +0000)]
Meta no longer raise a failure. Instead they return an empty set of
constraints. This is just a temporary patch. To be understood.

20 years ago- reindented
Claudio Sacerdoti Coen [Mon, 8 Mar 2004 23:16:50 +0000 (23:16 +0000)]
- reindented
- "count (" is not valid SQL (at least for MySql).
  Replaced with "count("
- binary removed. Tables are now binary by default.
  The advantage is that in this way indexes do work.

20 years agoDisambiguation can now return more than one choice.
Claudio Sacerdoti Coen [Mon, 8 Mar 2004 16:39:56 +0000 (16:39 +0000)]
Disambiguation can now return more than one choice.

20 years agoQuick & dirty patch to overcome a bug of ocamlfind.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 18:27:37 +0000 (18:27 +0000)]
Quick & dirty patch to overcome a bug of ocamlfind.

20 years agoAdded option -timeout. Default is 5s.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 17:57:39 +0000 (17:57 +0000)]
Added option -timeout. Default is 5s.

20 years ago\Assign and \subst to match the parser.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 17:54:15 +0000 (17:54 +0000)]
\Assign and \subst to match the parser.

20 years agoMutCase branches must be parsed and printed using \Rightarrow.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 17:51:45 +0000 (17:51 +0000)]
MutCase branches must be parsed and printed using \Rightarrow.

20 years agoBranch of MutCase 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.

20 years agoDebugging message removed.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:43:46 +0000 (16:43 +0000)]
Debugging message removed.

20 years agoapply_subst did not apply the substitution to the explicit named substitution
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.

20 years agoRefine now raises only RefineFailure, AssertFailure or Uncertain.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:20:42 +0000 (16:20 +0000)]
Refine now raises only RefineFailure, AssertFailure or Uncertain.

20 years agoWrong error message patched.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 16:20:29 +0000 (16:20 +0000)]
Wrong error message patched.

20 years agoList.nth not guarded by try ... with. Fixed.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 15:29:20 +0000 (15:29 +0000)]
List.nth not guarded by try ... with. Fixed.

20 years agoDebugging code removed.
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.

20 years agoHelmLogger logging function connected to MathQL Interpreter logger function.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 14:19:42 +0000 (14:19 +0000)]
HelmLogger logging function connected to MathQL Interpreter logger function.

20 years agoSyntax of explicit named substitions syncronized with the parser.
Claudio Sacerdoti Coen [Fri, 5 Mar 2004 12:24:05 +0000 (12:24 +0000)]
Syntax of explicit named substitions syncronized with the parser.

20 years agoYet another error in the id regexp: numbers are allowed in identifiers, as well
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.

20 years agoBug in guarded_by_destructors (case Rel to a definition in the context) fixed.
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.

20 years agoBig bug fixed: batchParser applied the varsprefix prefix also to
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.

20 years agoImproved output when [ MANY ] occurs.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 18:30:25 +0000 (18:30 +0000)]
Improved output when [ MANY ] occurs.

20 years ago...
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 17:54:40 +0000 (17:54 +0000)]
...

20 years ago...
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 17:39:57 +0000 (17:39 +0000)]
...

20 years ago- Improved error messaging.
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!

20 years ago- ported to latest CicAst.Ident format (Some [] <> None)
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

20 years agodifferentieted empty substitution list from no substitution given
Stefano Zacchiroli [Tue, 2 Mar 2004 17:12:58 +0000 (17:12 +0000)]
differentieted empty substitution list from no substitution given

20 years ago- regtest now handles more than one interpretation: the tests committed
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

20 years agoadded cast concrete syntax
Stefano Zacchiroli [Tue, 2 Mar 2004 15:53:19 +0000 (15:53 +0000)]
added cast concrete syntax

20 years agoThe regression tests now check also the generated disambiguation environments.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 15:19:06 +0000 (15:19 +0000)]
The regression tests now check also the generated disambiguation environments.

20 years agoRegtest fixed. It can now work also with multiple answers.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 14:53:13 +0000 (14:53 +0000)]
Regtest fixed. It can now work also with multiple answers.

20 years agoThe disambiguation now returns a list of interpretations.
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.

20 years agoThe disambiguation now returns a list of interpretations.
Claudio Sacerdoti Coen [Tue, 2 Mar 2004 13:18:13 +0000 (13:18 +0000)]
The disambiguation now returns a list of interpretations.

20 years agonow database interfaces are more abstract
Ferruccio Guidi [Fri, 27 Feb 2004 14:06:41 +0000 (14:06 +0000)]
now database interfaces are more abstract

20 years ago- MySQL mode added to the interpreter
Ferruccio Guidi [Thu, 26 Feb 2004 17:05:53 +0000 (17:05 +0000)]
- MySQL mode added to the interpreter
- hxp restored

20 years agoError message fixed.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:55:44 +0000 (16:55 +0000)]
Error message fixed.

20 years ago...
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:34:25 +0000 (16:34 +0000)]
...

20 years agotriciclo.conf.xml ==> gTopLevel.conf.xml
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:32:43 +0000 (16:32 +0000)]
triciclo.conf.xml ==> gTopLevel.conf.xml

20 years agoAdded () to MQInit.init.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:29:38 +0000 (16:29 +0000)]
Added () to MQInit.init.

20 years agoNew implementation of eat_prods. Some residual problems disappear.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 16:18:15 +0000 (16:18 +0000)]
New implementation of eat_prods. Some residual problems disappear.

20 years agoNew implementation of eat_prods.
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.

20 years ago- better handling of temp files wrt to failures. When a temp file has
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

20 years agoadded support for commands and scripts
Stefano Zacchiroli [Thu, 26 Feb 2004 14:53:18 +0000 (14:53 +0000)]
added support for commands and scripts

20 years agoadded vim modeline for encoding=utf8
Stefano Zacchiroli [Thu, 26 Feb 2004 14:52:57 +0000 (14:52 +0000)]
added vim modeline for encoding=utf8

20 years agoadded command and script ASTs with _debugging_only_ pretty printers
Stefano Zacchiroli [Thu, 26 Feb 2004 14:52:16 +0000 (14:52 +0000)]
added command and script ASTs with _debugging_only_ pretty printers

20 years agoBug fixed: names of just one character were not inserted into the objectName.
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.

20 years agoOne MQInterpreter commit broke regtest.ml. Fixed.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 12:51:01 +0000 (12:51 +0000)]
One MQInterpreter commit broke regtest.ml. Fixed.

20 years agoOptimization: since an invariant says that the inferred type of a term is
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).

20 years ago...
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 11:45:02 +0000 (11:45 +0000)]
...

20 years agoeqT removed.
Claudio Sacerdoti Coen [Thu, 26 Feb 2004 11:42:25 +0000 (11:42 +0000)]
eqT removed.

20 years agoVariable redefined. Fixed.
Claudio Sacerdoti Coen [Wed, 25 Feb 2004 11:27:00 +0000 (11:27 +0000)]
Variable redefined. Fixed.

20 years agoadded mathitaGui.mli
Stefano Zacchiroli [Tue, 24 Feb 2004 17:33:53 +0000 (17:33 +0000)]
added mathitaGui.mli

20 years agosnapshot
Stefano Zacchiroli [Tue, 24 Feb 2004 17:30:06 +0000 (17:30 +0000)]
snapshot

20 years agoadded functions and uris for binary {positive,integer}
Stefano Zacchiroli [Tue, 24 Feb 2004 16:09:38 +0000 (16:09 +0000)]
added functions and uris for binary {positive,integer}

20 years agoadded binary {positive,integer} notation
Stefano Zacchiroli [Tue, 24 Feb 2004 16:09:10 +0000 (16:09 +0000)]
added binary {positive,integer} notation