]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 12:57:29 +0000 (12:57 +0000)]
gt URL pointed to lt
Enrico Tassi [Fri, 23 Apr 2004 10:37:00 +0000 (10:37 +0000)]
Universes introduction
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 10:03:12 +0000 (10:03 +0000)]
rdfly hardcoded URL changed from mowgli.cs.unibo.it to localhost
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 17:00:31 +0000 (17:00 +0000)]
expandasking parameter passed to UWOBO.
Stefano Zacchiroli [Thu, 22 Apr 2004 16:33:02 +0000 (16:33 +0000)]
snapshot
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 15:02:50 +0000 (15:02 +0000)]
mysql_connection.* keys added
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 15:00:11 +0000 (15:00 +0000)]
mathql_interpreter.mysql_connection.* keys added.
Stefano Zacchiroli [Thu, 22 Apr 2004 13:54:12 +0000 (13:54 +0000)]
added (and used) some type shorthands
Stefano Zacchiroli [Thu, 22 Apr 2004 13:53:49 +0000 (13:53 +0000)]
- added some type shorthands
- added license information
Stefano Zacchiroli [Thu, 22 Apr 2004 13:53:22 +0000 (13:53 +0000)]
rebuit
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 12:38:16 +0000 (12:38 +0000)]
Patches to generate ?1 : ?2 : Type in place of ?1 : Type removed.
It is interesting to understand whether it is still necessary (after
the CicUnification bug fix) or not.
Enrico Tassi [Thu, 22 Apr 2004 12:33:35 +0000 (12:33 +0000)]
Big bug fixed: in the case t <?= ?1, the instantiation ?1 := t was generated
and then t : C and ?1 : E were retrieved/computed correctly; then
E <?= T was incorrectly tested (instead of T <?= E).
Enrico Tassi [Thu, 22 Apr 2004 11:29:14 +0000 (11:29 +0000)]
fourier.mli addedto interface files.
Stefano Zacchiroli [Thu, 22 Apr 2004 10:41:14 +0000 (10:41 +0000)]
snapshot
Stefano Zacchiroli [Thu, 22 Apr 2004 09:36:54 +0000 (09:36 +0000)]
added /help method (needed by respawner)
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 09:11:16 +0000 (09:11 +0000)]
IMPLEMENTATION_FILES now generated from INTERFACE_FILES.
Stefano Zacchiroli [Thu, 22 Apr 2004 08:31:19 +0000 (08:31 +0000)]
added .cvsignore
Stefano Zacchiroli [Wed, 21 Apr 2004 17:46:17 +0000 (17:46 +0000)]
detects and uses {ocamlc,ocamlopt}.opt when available
Stefano Zacchiroli [Wed, 21 Apr 2004 17:35:00 +0000 (17:35 +0000)]
detect and use {ocamlc,ocamlopt}.opt when they are available
Stefano Zacchiroli [Wed, 21 Apr 2004 17:29:35 +0000 (17:29 +0000)]
exported term_of_uri
Stefano Zacchiroli [Wed, 21 Apr 2004 17:26:39 +0000 (17:26 +0000)]
added helmLibraryObjects.mli mention
Stefano Zacchiroli [Wed, 21 Apr 2004 16:36:38 +0000 (16:36 +0000)]
added .mli
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:53 +0000 (17:00 +0000)]
got rid of a ~status label
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:27 +0000 (17:00 +0000)]
got rid of ~status label
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:07 +0000 (17:00 +0000)]
got rid of ~status label so that tactics can now be applied partially,
delta reduced, ...
Stefano Zacchiroli [Tue, 20 Apr 2004 09:41:10 +0000 (09:41 +0000)]
added ocamlfind library checks to configure.ac
Stefano Zacchiroli [Tue, 20 Apr 2004 09:27:36 +0000 (09:27 +0000)]
renamed mathita to matita
Stefano Zacchiroli [Tue, 20 Apr 2004 08:54:23 +0000 (08:54 +0000)]
snapshot
Stefano Zacchiroli [Mon, 19 Apr 2004 12:12:35 +0000 (12:12 +0000)]
ignore Makefile since now it's generated by configure
Stefano Zacchiroli [Mon, 19 Apr 2004 12:12:16 +0000 (12:12 +0000)]
added Makefile.in
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:37 +0000 (12:10 +0000)]
reorganized metas so that pxp is references only through helm-pxp
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:20 +0000 (12:10 +0000)]
added hbugs' (client) meta
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:03 +0000 (12:10 +0000)]
generalized META.* ignoring
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
Stefano Zacchiroli [Mon, 19 Apr 2004 12:08:35 +0000 (12:08 +0000)]
- use PxpHelmConf
- no longer use deprecated Pxp_yacc module
Stefano Zacchiroli [Mon, 19 Apr 2004 12:08:13 +0000 (12:08 +0000)]
- use PxpHelmConf
- no longer use deprecated Pxp_yacc
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:51 +0000 (12:07 +0000)]
use PxpHelmConf
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:37 +0000 (12:07 +0000)]
added dep on Helm_registry
Stefano Zacchiroli [Mon, 19 Apr 2004 12:07:12 +0000 (12:07 +0000)]
use PxpHelmConf module
Stefano Zacchiroli [Mon, 19 Apr 2004 12:06:56 +0000 (12:06 +0000)]
- use PxpHelmConf
- removed references to deprecated Pxp_yacc module
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
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)
Stefano Zacchiroli [Mon, 19 Apr 2004 12:04:26 +0000 (12:04 +0000)]
injected hbugs under ocaml/ dir
Stefano Zacchiroli [Mon, 19 Apr 2004 12:01:03 +0000 (12:01 +0000)]
moved hbugs under ocaml/
Stefano Zacchiroli [Mon, 19 Apr 2004 08:38:12 +0000 (08:38 +0000)]
fixed a typo (inside a comment)
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.
Stefano Zacchiroli [Fri, 16 Apr 2004 16:39:14 +0000 (16:39 +0000)]
use respawner
Stefano Zacchiroli [Fri, 16 Apr 2004 16:39:01 +0000 (16:39 +0000)]
changed logging message
Stefano Zacchiroli [Fri, 16 Apr 2004 16:16:36 +0000 (16:16 +0000)]
removed deprecated uwobo_forever.sh
Stefano Zacchiroli [Fri, 16 Apr 2004 16:16:01 +0000 (16:16 +0000)]
removed tedious "_mowgli" postfix
Stefano Zacchiroli [Fri, 16 Apr 2004 16:02:38 +0000 (16:02 +0000)]
use new daemon_respawner.sh
Stefano Zacchiroli [Fri, 16 Apr 2004 16:02:27 +0000 (16:02 +0000)]
fixed some typos in sample init.d
Stefano Zacchiroli [Fri, 16 Apr 2004 15:56:20 +0000 (15:56 +0000)]
added generic daemon respawner
Stefano Zacchiroli [Fri, 16 Apr 2004 15:56:08 +0000 (15:56 +0000)]
script deprecated
Stefano Zacchiroli [Fri, 16 Apr 2004 12:16:08 +0000 (12:16 +0000)]
added newline to log when log_file is in use
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
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
Stefano Zacchiroli [Fri, 16 Apr 2004 08:18:07 +0000 (08:18 +0000)]
- rewritten http_getter logger interface
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)
Andrea Asperti [Thu, 15 Apr 2004 16:47:42 +0000 (16:47 +0000)]
Metasenv added as parameter to eta_fixing.
Stefano Zacchiroli [Thu, 15 Apr 2004 13:36:31 +0000 (13:36 +0000)]
s/dtd_base_url/dtd_base_urls/
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
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
Stefano Zacchiroli [Thu, 15 Apr 2004 13:35:00 +0000 (13:35 +0000)]
- better pretty printing on /update
- added stdout logger
Stefano Zacchiroli [Thu, 15 Apr 2004 12:52:24 +0000 (12:52 +0000)]
added string_of_html_tag (plain text pretty printer for tags)
Stefano Zacchiroli [Thu, 15 Apr 2004 12:25:40 +0000 (12:25 +0000)]
added support for multiple dtd_base_urls
Ferruccio Guidi [Wed, 14 Apr 2004 17:33:12 +0000 (17:33 +0000)]
updating all sections
Ferruccio Guidi [Wed, 14 Apr 2004 16:07:10 +0000 (16:07 +0000)]
patched
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!
Stefano Zacchiroli [Wed, 14 Apr 2004 13:56:47 +0000 (13:56 +0000)]
added exists_meta
Ferruccio Guidi [Wed, 14 Apr 2004 11:25:09 +0000 (11:25 +0000)]
patched
Ferruccio Guidi [Tue, 13 Apr 2004 15:58:12 +0000 (15:58 +0000)]
updating the introduction
Stefano Zacchiroli [Fri, 9 Apr 2004 15:09:28 +0000 (15:09 +0000)]
ported to latest polymorphic variant types
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.
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).
Stefano Zacchiroli [Wed, 7 Apr 2004 12:42:37 +0000 (12:42 +0000)]
added a missing <br> tag
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:51 +0000 (12:43 +0000)]
implemented save_to
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
Stefano Zacchiroli [Tue, 6 Apr 2004 12:43:02 +0000 (12:43 +0000)]
added Unix dependency (needed in order to run xmllint)
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.
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.
Stefano Zacchiroli [Tue, 6 Apr 2004 09:56:08 +0000 (09:56 +0000)]
- added test file
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)
Stefano Zacchiroli [Tue, 6 Apr 2004 09:52:10 +0000 (09:52 +0000)]
- use polymorphic variants for some configuration parameters
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
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).
Stefano Zacchiroli [Tue, 6 Apr 2004 09:02:18 +0000 (09:02 +0000)]
reorganized functions order
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
Stefano Zacchiroli [Mon, 5 Apr 2004 17:22:29 +0000 (17:22 +0000)]
added html_of_html_tag
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.
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).
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
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.
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
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)
Stefano Zacchiroli [Thu, 1 Apr 2004 17:06:27 +0000 (17:06 +0000)]
removed no longer needed password from connection string
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)
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
Claudio Sacerdoti Coen [Thu, 1 Apr 2004 16:40:46 +0000 (16:40 +0000)]
<VARIABLE as="LocalFact"/> added
Stefano Zacchiroli [Thu, 1 Apr 2004 15:45:08 +0000 (15:45 +0000)]
removed an out of date comment