]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agofixed a typo (inside a comment)
Stefano Zacchiroli [Mon, 19 Apr 2004 08:38:12 +0000 (08:38 +0000)]
fixed a typo (inside a comment)

20 years agotest_equality_only was not used in sort comparison.
Claudio Sacerdoti Coen [Fri, 16 Apr 2004 17:15:35 +0000 (17:15 +0000)]
test_equality_only was not used in sort comparison.
It should be implemented only in unification.

20 years agouse respawner
Stefano Zacchiroli [Fri, 16 Apr 2004 16:39:14 +0000 (16:39 +0000)]
use respawner

20 years agochanged logging message
Stefano Zacchiroli [Fri, 16 Apr 2004 16:39:01 +0000 (16:39 +0000)]
changed logging message

20 years agoremoved deprecated uwobo_forever.sh
Stefano Zacchiroli [Fri, 16 Apr 2004 16:16:36 +0000 (16:16 +0000)]
removed deprecated uwobo_forever.sh

20 years agoremoved tedious "_mowgli" postfix
Stefano Zacchiroli [Fri, 16 Apr 2004 16:16:01 +0000 (16:16 +0000)]
removed tedious "_mowgli" postfix

20 years agouse new daemon_respawner.sh
Stefano Zacchiroli [Fri, 16 Apr 2004 16:02:38 +0000 (16:02 +0000)]
use new daemon_respawner.sh

20 years agofixed some typos in sample init.d
Stefano Zacchiroli [Fri, 16 Apr 2004 16:02:27 +0000 (16:02 +0000)]
fixed some typos in sample init.d

20 years agoadded generic daemon respawner
Stefano Zacchiroli [Fri, 16 Apr 2004 15:56:20 +0000 (15:56 +0000)]
added generic daemon respawner

20 years agoscript deprecated
Stefano Zacchiroli [Fri, 16 Apr 2004 15:56:08 +0000 (15:56 +0000)]
script deprecated

20 years agoadded newline to log when log_file is in use
Stefano Zacchiroli [Fri, 16 Apr 2004 12:16:08 +0000 (12:16 +0000)]
added newline to log when log_file is in use

20 years ago- addead autoconf-iguration. Actually it only set the default runtime
Stefano Zacchiroli [Fri, 16 Apr 2004 08:43:20 +0000 (08:43 +0000)]
- addead autoconf-iguration. Actually it only set the default runtime
  configuration file

20 years ago- use new logger interface
Stefano Zacchiroli [Fri, 16 Apr 2004 08:18:39 +0000 (08:18 +0000)]
- use new logger interface
- added support for log_level and log_file in configuration file

20 years ago- rewritten http_getter logger interface
Stefano Zacchiroli [Fri, 16 Apr 2004 08:18:07 +0000 (08:18 +0000)]
- rewritten http_getter logger interface

20 years ago- added sample usage of get_opt method
Stefano Zacchiroli [Fri, 16 Apr 2004 08:17:38 +0000 (08:17 +0000)]
- added sample usage of get_opt method
- added method get_opt_default (like get_opt with an additional default
  value)

20 years agoMetasenv added as parameter to eta_fixing.
Andrea Asperti [Thu, 15 Apr 2004 16:47:42 +0000 (16:47 +0000)]
Metasenv added as parameter to eta_fixing.

20 years agos/dtd_base_url/dtd_base_urls/
Stefano Zacchiroli [Thu, 15 Apr 2004 13:36:31 +0000 (13:36 +0000)]
s/dtd_base_url/dtd_base_urls/

20 years ago- better pretty printing of exceptions (added red color)
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:53 +0000 (13:35 +0000)]
- better pretty printing of exceptions (added red color)
- added "-update" command line parameter for batch updating

20 years ago- fixed dtd_base_urls implementation
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:21 +0000 (13:35 +0000)]
- fixed dtd_base_urls implementation
- factorized a lot of code in document patching

20 years ago- better pretty printing on /update
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:00 +0000 (13:35 +0000)]
- better pretty printing on /update
- added stdout logger

20 years agoadded string_of_html_tag (plain text pretty printer for tags)
Stefano Zacchiroli [Thu, 15 Apr 2004 12:52:24 +0000 (12:52 +0000)]
added string_of_html_tag (plain text pretty printer for tags)

20 years agoadded support for multiple dtd_base_urls
Stefano Zacchiroli [Thu, 15 Apr 2004 12:25:40 +0000 (12:25 +0000)]
added support for multiple dtd_base_urls

20 years agoupdating all sections
Ferruccio Guidi [Wed, 14 Apr 2004 17:33:12 +0000 (17:33 +0000)]
updating all sections

20 years agopatched
Ferruccio Guidi [Wed, 14 Apr 2004 16:07:10 +0000 (16:07 +0000)]
patched

20 years agoBug fixed: the following happened.
Claudio Sacerdoti Coen [Wed, 14 Apr 2004 14:11:52 +0000 (14:11 +0000)]
Bug fixed: the following happened.
Auto generated two goals.
Closing the first goal instantiated also the second goal.
But we were still iterating over the original list of goals ==> BOOM!

20 years agoadded exists_meta
Stefano Zacchiroli [Wed, 14 Apr 2004 13:56:47 +0000 (13:56 +0000)]
added exists_meta

20 years agopatched
Ferruccio Guidi [Wed, 14 Apr 2004 11:25:09 +0000 (11:25 +0000)]
patched

20 years agoupdating the introduction
Ferruccio Guidi [Tue, 13 Apr 2004 15:58:12 +0000 (15:58 +0000)]
updating the introduction

20 years agoported to latest polymorphic variant types
Stefano Zacchiroli [Fri, 9 Apr 2004 15:09:28 +0000 (15:09 +0000)]
ported to latest polymorphic variant types

20 years agoAdded flag test_equality_only to are_convertible to better implement
Claudio Sacerdoti Coen [Wed, 7 Apr 2004 14:30:41 +0000 (14:30 +0000)]
Added flag test_equality_only to are_convertible to better implement
the <=_{\beta\delta\iota\zeta} relation.

20 years agoAdded flag test_equality_only to are_convertible (to better implement
Claudio Sacerdoti Coen [Wed, 7 Apr 2004 14:29:25 +0000 (14:29 +0000)]
Added flag test_equality_only to are_convertible (to better implement
the <=_{\beta\delta\iota\zeta} relation).

20 years agoadded a missing <br> tag
Stefano Zacchiroli [Wed, 7 Apr 2004 12:42:37 +0000 (12:42 +0000)]
added a missing <br> tag

20 years agoimplemented save_to
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:51 +0000 (12:43 +0000)]
implemented save_to

20 years ago- uncommented save_to function (now implemented)
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:43 +0000 (12:43 +0000)]
- uncommented save_to function (now implemented)
- added (tiny) description of the 'variable interpolation' feature

20 years agoadded Unix dependency (needed in order to run xmllint)
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:02 +0000 (12:43 +0000)]
added Unix dependency (needed in order to run xmllint)

20 years agoeta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
Stefano Zacchiroli [Tue, 6 Apr 2004 12:38:20 +0000 (12:38 +0000)]
eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing.

20 years agoThe parser accepts terms with metavariables as statements of theorems ==>
Stefano Zacchiroli [Tue, 6 Apr 2004 12:08:23 +0000 (12:08 +0000)]
The parser accepts terms with metavariables as statements of theorems ==>
metavariable instantiation must be propagated also on the theorem statement.

20 years ago- added test file
Stefano Zacchiroli [Tue, 6 Apr 2004 09:56:08 +0000 (09:56 +0000)]
- added test file

20 years ago- added via_http parameter so that when the getter is used locally (i.e.
Stefano Zacchiroli [Tue, 6 Apr 2004 09:53:26 +0000 (09:53 +0000)]
- added via_http parameter so that when the getter is used locally (i.e.
  as a library), http specific messages aren't generated
- use polymorphic variants for some configuration parameters
- better logging on /update (<br> tags are now generated)

20 years ago- use polymorphic variants for some configuration parameters
Stefano Zacchiroli [Tue, 6 Apr 2004 09:52:10 +0000 (09:52 +0000)]
- use polymorphic variants for some configuration parameters

20 years agobugfix: local context and canonical context previously don't have the
Stefano Zacchiroli [Tue, 6 Apr 2004 09:50:39 +0000 (09:50 +0000)]
bugfix: local context and canonical context previously don't have the
same length

20 years agobugfix: the function that abstract constant occurrences by putting metavariables
Stefano Zacchiroli [Tue, 6 Apr 2004 09:04:45 +0000 (09:04 +0000)]
bugfix: the function that abstract constant occurrences by putting metavariables
in place of identity explicit substitutions (local contexts) is generalized to
put ?1 : ?2 : Type in place of a ?1 : Type to take care of <Type in contravariant
position. Note: this is still partially bugged (see previous commit on the same
topic).

20 years agoreorganized functions order
Stefano Zacchiroli [Tue, 6 Apr 2004 09:02:18 +0000 (09:02 +0000)]
reorganized functions order

20 years agohttp_getter.conf.xml ==> /projects/helm/etc/http_getter.conf.xml
Claudio Sacerdoti Coen [Mon, 5 Apr 2004 17:32:45 +0000 (17:32 +0000)]
http_getter.conf.xml ==> /projects/helm/etc/http_getter.conf.xml

20 years agoadded html_of_html_tag
Stefano Zacchiroli [Mon, 5 Apr 2004 17:22:29 +0000 (17:22 +0000)]
added html_of_html_tag

20 years agoURL patching in ENTITY declarations extended to cover also absolute URLs.
Claudio Sacerdoti Coen [Mon, 5 Apr 2004 16:57:44 +0000 (16:57 +0000)]
URL patching in ENTITY declarations extended to cover also absolute URLs.

20 years agoXHTML character entities (used in the internal subset of .theory.xml files).
Claudio Sacerdoti Coen [Mon, 5 Apr 2004 16:49:13 +0000 (16:49 +0000)]
XHTML character entities (used in the internal subset of .theory.xml files).

20 years agoAdded a new function in_cache to cicEnvironemt. It takes an uri
Andrea Asperti [Mon, 5 Apr 2004 13:58:54 +0000 (13:58 +0000)]
Added a new function in_cache to cicEnvironemt. It takes an uri
and returns true or false according to the fact that uri is or
is not in the cache

20 years agoht:DEFINITION/Definition differentiated into
Claudio Sacerdoti Coen [Sun, 4 Apr 2004 13:44:08 +0000 (13:44 +0000)]
ht:DEFINITION/Definition differentiated into
 ht:DEFINITION/Definition and
 ht:DEFINITION/InteractiveDefinition

because of an explicit request of Iris Loeb.

20 years agos/per_user_settings/user_settings/ for consistency with gTopLevel
Stefano Zacchiroli [Fri, 2 Apr 2004 12:20:14 +0000 (12:20 +0000)]
s/per_user_settings/user_settings/ for consistency with gTopLevel
configuration file

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.