]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years ago- reordered modules so that pxp could be used as entry point for pxp
Stefano Zacchiroli [Mon, 19 Apr 2004 12:09:22 +0000 (12:09 +0000)]
- reordered modules so that pxp could be used as entry point for pxp
- added hbugs
- pretty printed modules

20 years ago- use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:08:35 +0000 (12:08 +0000)]
- use PxpHelmConf
- no longer use deprecated Pxp_yacc module

20 years ago- use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:08:13 +0000 (12:08 +0000)]
- use PxpHelmConf
- no longer use deprecated Pxp_yacc

20 years agouse PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:51 +0000 (12:07 +0000)]
use PxpHelmConf

20 years agoadded dep on Helm_registry
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:37 +0000 (12:07 +0000)]
added dep on Helm_registry

20 years agouse PxpHelmConf module
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:12 +0000 (12:07 +0000)]
use PxpHelmConf module

20 years ago- use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:06:56 +0000 (12:06 +0000)]
- use PxpHelmConf
- removed references to deprecated Pxp_yacc module

20 years ago- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
Stefano Zacchiroli [Mon, 19 Apr 2004 12:06:25 +0000 (12:06 +0000)]
- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
  belongs to Getter module!)
- added PxpHelmConf module, repository of Pxp configurations for helm

20 years agoadded ExtThread module, ex Hbugs_deity (a Thread module with killing
Stefano Zacchiroli [Mon, 19 Apr 2004 12:05:30 +0000 (12:05 +0000)]
added ExtThread module, ex Hbugs_deity (a Thread module with killing
capabilities)

20 years agoinjected hbugs under ocaml/ dir
Stefano Zacchiroli [Mon, 19 Apr 2004 12:04:26 +0000 (12:04 +0000)]
injected hbugs under ocaml/ dir

20 years agomoved hbugs under ocaml/
Stefano Zacchiroli [Mon, 19 Apr 2004 12:01:03 +0000 (12:01 +0000)]
moved hbugs under ocaml/

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