]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agoThis commit was manufactured by cvs2svn to create tag 'V_0_5_1_3'. V_0_5_1_3
no author [Thu, 22 Jan 2004 11:59:18 +0000 (11:59 +0000)]
This commit was manufactured by cvs2svn to create tag 'V_0_5_1_3'.

20 years ago- removed some unneeded dependencies from debian/control
Stefano Zacchiroli [Thu, 22 Jan 2004 11:59:18 +0000 (11:59 +0000)]
- removed some unneeded dependencies from debian/control
- bumped standards-version

20 years agoTypo fixed.
Claudio Sacerdoti Coen [Thu, 22 Jan 2004 11:19:26 +0000 (11:19 +0000)]
Typo fixed.

20 years agoprettified
Stefano Zacchiroli [Thu, 22 Jan 2004 10:44:37 +0000 (10:44 +0000)]
prettified

20 years agouse new proofEngineHelpers
Stefano Zacchiroli [Thu, 22 Jan 2004 10:41:40 +0000 (10:41 +0000)]
use new proofEngineHelpers

20 years agomoved hard coded uris to HelmLibraryObjects
Stefano Zacchiroli [Thu, 22 Jan 2004 10:33:10 +0000 (10:33 +0000)]
moved hard coded uris to HelmLibraryObjects

20 years agoported to cicMetaSubst
Stefano Zacchiroli [Thu, 22 Jan 2004 10:32:52 +0000 (10:32 +0000)]
ported to cicMetaSubst

20 years ago- splitted into cicMetaSubst
Stefano Zacchiroli [Thu, 22 Jan 2004 10:31:33 +0000 (10:31 +0000)]
- splitted into cicMetaSubst
- bugfixes
- better exceptions

20 years agobugfixes, typos and the hell
Stefano Zacchiroli [Thu, 22 Jan 2004 10:30:52 +0000 (10:30 +0000)]
bugfixes, typos and the hell

20 years agosplit into this and cicMetaSubst.mli
Stefano Zacchiroli [Thu, 22 Jan 2004 10:29:33 +0000 (10:29 +0000)]
split into this and cicMetaSubst.mli

20 years agoadded CicMetaSubst module for metavariable instantiatiation
Stefano Zacchiroli [Thu, 22 Jan 2004 10:28:34 +0000 (10:28 +0000)]
added CicMetaSubst module for metavariable instantiatiation

20 years agobetter exception and error messages
Stefano Zacchiroli [Thu, 22 Jan 2004 10:26:32 +0000 (10:26 +0000)]
better exception and error messages

20 years ago- bugfix: print metas local context in the rigth order
Stefano Zacchiroli [Thu, 22 Jan 2004 10:24:50 +0000 (10:24 +0000)]
- bugfix: print metas local context in the rigth order
- renamed string_of_name to ppname and exported it

20 years agoFirst version of refine for MutCase, still largely incomplete.
Andrea Asperti [Tue, 20 Jan 2004 10:25:10 +0000 (10:25 +0000)]
First version of refine for MutCase, still largely incomplete.

20 years ago/projects/helm/log moved to /var/log/mowgli
Claudio Sacerdoti Coen [Tue, 20 Jan 2004 08:40:09 +0000 (08:40 +0000)]
/projects/helm/log moved to /var/log/mowgli

20 years ago/projects/helm/run/*_mowgli.pid moved into /var/run
Claudio Sacerdoti Coen [Tue, 20 Jan 2004 08:38:35 +0000 (08:38 +0000)]
/projects/helm/run/*_mowgli.pid moved into /var/run

20 years agoScripts simplified (since now we have only one cluster and only one
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 17:41:47 +0000 (17:41 +0000)]
Scripts simplified (since now we have only one cluster and only one
stable version of the library).

20 years agoNuPRL stuff moved.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 17:41:25 +0000 (17:41 +0000)]
NuPRL stuff moved.

20 years agoNo longer in use. The official repository for the
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 15:25:01 +0000 (15:25 +0000)]
No longer in use. The official repository for the
stylesheet is now the repository of mowgli.

20 years agoBranch V7_3_new_exportation merged.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 15:13:45 +0000 (15:13 +0000)]
Branch V7_3_new_exportation merged.

20 years agoError message updated.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:32:08 +0000 (14:32 +0000)]
Error message updated.

20 years agoNo more in use.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:31:29 +0000 (14:31 +0000)]
No more in use.

20 years agoTypo fixed.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:26:46 +0000 (14:26 +0000)]
Typo fixed.

20 years agoWe are now using the standard dot distribution of debian.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 14:26:22 +0000 (14:26 +0000)]
We are now using the standard dot distribution of debian.

20 years agoOnly V7_mowgli left.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 13:43:48 +0000 (13:43 +0000)]
Only V7_mowgli left.

20 years agoDaemons moved to /projects/helm/daemons.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:57:29 +0000 (12:57 +0000)]
Daemons moved to /projects/helm/daemons.

20 years agoDaemon moved to /projects/helm/daemons.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:41:15 +0000 (12:41 +0000)]
Daemon moved to /projects/helm/daemons.

20 years ago*** empty log message ***
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:36:02 +0000 (12:36 +0000)]
*** empty log message ***

20 years agoSeveral daemons moved into /projects/helm/daemons.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:35:23 +0000 (12:35 +0000)]
Several daemons moved into /projects/helm/daemons.

20 years agoErrore message improved.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:10:48 +0000 (12:10 +0000)]
Errore message improved.

20 years agoMissing package dependency.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 12:02:42 +0000 (12:02 +0000)]
Missing package dependency.

20 years agosnapshot, almost working
Stefano Zacchiroli [Mon, 19 Jan 2004 11:43:03 +0000 (11:43 +0000)]
snapshot, almost working
TODO:
- domain processing order
- notation generation

20 years agoadded a CSC's TODO comment
Stefano Zacchiroli [Mon, 19 Jan 2004 11:41:56 +0000 (11:41 +0000)]
added a CSC's TODO comment

20 years agoadded MkImplicit module for meta handling
Stefano Zacchiroli [Mon, 19 Jan 2004 11:39:59 +0000 (11:39 +0000)]
added MkImplicit module for meta handling

20 years agoadded Peano module and functions to create natural/real terms
Stefano Zacchiroli [Mon, 19 Jan 2004 11:38:41 +0000 (11:38 +0000)]
added Peano module and functions to create natural/real terms

20 years agoBranch V7_3_new_exportation closed.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 11:28:09 +0000 (11:28 +0000)]
Branch V7_3_new_exportation closed.

20 years agomathql listed twice
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 10:39:17 +0000 (10:39 +0000)]
mathql listed twice

20 years agoThe searchengine now requires the mathql_db_map.txt.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 10:12:48 +0000 (10:12 +0000)]
The searchengine now requires the mathql_db_map.txt.
Added the mathql_db_map.txt file and the new environment variable
MATHQL_DB_MAP.

20 years agoNo longer in use.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 09:54:59 +0000 (09:54 +0000)]
No longer in use.

20 years agoError in the warning message.
Claudio Sacerdoti Coen [Mon, 19 Jan 2004 09:52:20 +0000 (09:52 +0000)]
Error in the warning message.

20 years agoadded missing depending on (CSC's) helm-cic_textual_parser
Stefano Zacchiroli [Wed, 14 Jan 2004 18:07:41 +0000 (18:07 +0000)]
added missing depending on (CSC's) helm-cic_textual_parser

20 years agoremoved ui_logger, now in external module logger
Stefano Zacchiroli [Wed, 14 Jan 2004 18:04:41 +0000 (18:04 +0000)]
removed ui_logger, now in external module logger

20 years agoadded missing dependencies on mathql-*
Stefano Zacchiroli [Wed, 14 Jan 2004 18:03:26 +0000 (18:03 +0000)]
added missing dependencies on mathql-*

20 years agoadded logger's META
Stefano Zacchiroli [Wed, 14 Jan 2004 18:01:32 +0000 (18:01 +0000)]
added logger's META

20 years agomoved to the logger module
Stefano Zacchiroli [Wed, 14 Jan 2004 17:59:01 +0000 (17:59 +0000)]
moved to the logger module

20 years ago- added logger module
Stefano Zacchiroli [Wed, 14 Jan 2004 17:57:59 +0000 (17:57 +0000)]
- added logger module
- vertical ordering

20 years agomoved here ui_logger from gTopLeve
Stefano Zacchiroli [Wed, 14 Jan 2004 17:57:11 +0000 (17:57 +0000)]
moved here ui_logger from gTopLeve

20 years agostill a working copy, now towards a cleaner implementation ...
Stefano Zacchiroli [Wed, 14 Jan 2004 17:54:33 +0000 (17:54 +0000)]
still a working copy, now towards a cleaner implementation ...

20 years agoadded HelmLibraryObjects module
Stefano Zacchiroli [Mon, 12 Jan 2004 17:12:39 +0000 (17:12 +0000)]
added HelmLibraryObjects module

20 years ago* removed email address
Luca Padovani [Fri, 19 Dec 2003 09:34:20 +0000 (09:34 +0000)]
* removed email address

20 years agoBug commented out. The comment is also commented.
Claudio Sacerdoti Coen [Thu, 18 Dec 2003 14:42:06 +0000 (14:42 +0000)]
Bug commented out. The comment is also commented.

20 years agoBig bug spotted: restriction can fail and it was implicitly assumed that it
Claudio Sacerdoti Coen [Thu, 18 Dec 2003 13:17:51 +0000 (13:17 +0000)]
Big bug spotted: restriction can fail and it was implicitly assumed that it
didn't. Added another comment in the code.

20 years agoOne of the bug I detected (and commented) in my last commit was not a bug.
Claudio Sacerdoti Coen [Thu, 18 Dec 2003 10:46:18 +0000 (10:46 +0000)]
One of the bug I detected (and commented) in my last commit was not a bug.
This commit removes the erroneus comment.

20 years agopatched
Ferruccio Guidi [Wed, 17 Dec 2003 18:36:03 +0000 (18:36 +0000)]
patched

20 years agoMore comments. Some of them may highlight bugs or open issues.
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 17:37:03 +0000 (17:37 +0000)]
More comments. Some of them may highlight bugs or open issues.

20 years agogenerate gui to temp file in order to catch lablgladecc2 failures
Stefano Zacchiroli [Wed, 17 Dec 2003 14:49:52 +0000 (14:49 +0000)]
generate gui to temp file in order to catch lablgladecc2 failures

20 years agorebuilt
Stefano Zacchiroli [Wed, 17 Dec 2003 14:41:28 +0000 (14:41 +0000)]
rebuilt

20 years agos/Logger/CicLogger/
Stefano Zacchiroli [Wed, 17 Dec 2003 14:11:32 +0000 (14:11 +0000)]
s/Logger/CicLogger/

20 years agouse ocaml-http instead of netclient for http requests
Stefano Zacchiroli [Wed, 17 Dec 2003 14:04:28 +0000 (14:04 +0000)]
use ocaml-http instead of netclient for http requests

20 years agoMakefiles patched
Ferruccio Guidi [Wed, 17 Dec 2003 11:52:28 +0000 (11:52 +0000)]
Makefiles patched

20 years agoBig bug spotted and commented: the delift function considers the explicit
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 11:49:58 +0000 (11:49 +0000)]
Big bug spotted and commented: the delift function considers the explicit
substitution over metavariable occurrences as telescopic. Instead it is
simultaneous.

20 years ago* comments improved an possible code weakness (i.e. less than first order
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 11:27:30 +0000 (11:27 +0000)]
* comments improved an possible code weakness (i.e. less than first order
  unification detected) made explicit in the comment and with a warning.

20 years ago* Reindentation
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 10:47:40 +0000 (10:47 +0000)]
* Reindentation
* More comments

20 years ago* Reindentation.
Claudio Sacerdoti Coen [Wed, 17 Dec 2003 10:46:18 +0000 (10:46 +0000)]
* Reindentation.
* Useless code elimination.
* Debug code elimination.

20 years ago- ported to new output_html Disambiguate callback
Stefano Zacchiroli [Tue, 16 Dec 2003 17:56:42 +0000 (17:56 +0000)]
- ported to new output_html Disambiguate callback
- removed netclient dependency

20 years agos/netclient/http/ in dependencies
Stefano Zacchiroli [Tue, 16 Dec 2003 17:56:03 +0000 (17:56 +0000)]
s/netclient/http/ in dependencies

20 years agocosmetic changes
Stefano Zacchiroli [Tue, 16 Dec 2003 17:55:44 +0000 (17:55 +0000)]
cosmetic changes

20 years agouse ocaml-http instead of netclient for http GET requests
Stefano Zacchiroli [Tue, 16 Dec 2003 17:37:58 +0000 (17:37 +0000)]
use ocaml-http instead of netclient for http GET requests

20 years ago- use ocaml-http instead of netclient for http GET requests
Stefano Zacchiroli [Tue, 16 Dec 2003 17:34:08 +0000 (17:34 +0000)]
- use ocaml-http instead of netclient for http GET requests
- renamed Makefile targets so that all and clean have the usual
  semantics

20 years agoremoved old perl versions of graph daemons
Stefano Zacchiroli [Tue, 16 Dec 2003 17:33:25 +0000 (17:33 +0000)]
removed old perl versions of graph daemons

20 years agouse new METAS/* names
Stefano Zacchiroli [Tue, 16 Dec 2003 17:31:04 +0000 (17:31 +0000)]
use new METAS/* names

20 years agoremoved ancient "interface" dir
Stefano Zacchiroli [Tue, 16 Dec 2003 17:19:48 +0000 (17:19 +0000)]
removed ancient "interface" dir

20 years agoremoved ancient lablgtk, lablgtk_gtkmathview
Stefano Zacchiroli [Tue, 16 Dec 2003 17:16:01 +0000 (17:16 +0000)]
removed ancient lablgtk, lablgtk_gtkmathview

20 years agoremoved ancient mlminidom
Stefano Zacchiroli [Tue, 16 Dec 2003 17:15:16 +0000 (17:15 +0000)]
removed ancient mlminidom

20 years agoremoved ancient pxp dir
Stefano Zacchiroli [Tue, 16 Dec 2003 17:14:45 +0000 (17:14 +0000)]
removed ancient pxp dir

20 years agoremoved useless ocamlfind query of the netclient package
Stefano Zacchiroli [Tue, 16 Dec 2003 17:11:48 +0000 (17:11 +0000)]
removed useless ocamlfind query of the netclient package

20 years agoremoved useless "-package netclient" from one of the examples
Stefano Zacchiroli [Tue, 16 Dec 2003 17:10:48 +0000 (17:10 +0000)]
removed useless "-package netclient" from one of the examples

20 years agobumped version to 0.0.9
Stefano Zacchiroli [Tue, 16 Dec 2003 17:02:01 +0000 (17:02 +0000)]
bumped version to 0.0.9

20 years agofixed typo in ocamldoc comment
Stefano Zacchiroli [Tue, 16 Dec 2003 17:01:28 +0000 (17:01 +0000)]
fixed typo in ocamldoc comment

20 years agoremoved dependency on netclient, use http_client module from ocaml-http
Stefano Zacchiroli [Tue, 16 Dec 2003 17:00:48 +0000 (17:00 +0000)]
removed dependency on netclient, use http_client module from ocaml-http

20 years agoadded parse_response_fst_line
Stefano Zacchiroli [Tue, 16 Dec 2003 16:49:38 +0000 (16:49 +0000)]
added parse_response_fst_line

20 years ago- return (or iter on) just http response's body
Stefano Zacchiroli [Tue, 16 Dec 2003 16:49:04 +0000 (16:49 +0000)]
- return (or iter on) just http response's body
- s/http_get_iter_buf/http_get_iter/
- commented interface files

20 years agoadded Malformed_response exception
Stefano Zacchiroli [Tue, 16 Dec 2003 16:48:02 +0000 (16:48 +0000)]
added Malformed_response exception

20 years agoadded http_client module
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:52 +0000 (16:17 +0000)]
added http_client module

20 years agorebuilt
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:40 +0000 (16:17 +0000)]
rebuilt

20 years agoported to ocaml 3.07
Stefano Zacchiroli [Tue, 16 Dec 2003 16:17:23 +0000 (16:17 +0000)]
ported to ocaml 3.07

20 years agorenamed META*.src to meta*.src so that ocamlfind list doesn't list both
Stefano Zacchiroli [Tue, 16 Dec 2003 16:06:35 +0000 (16:06 +0000)]
renamed META*.src to meta*.src so that ocamlfind list doesn't list both
src and real METAs

20 years ago- fixed logging in log window so that spurious html tags are no longer
Stefano Zacchiroli [Tue, 16 Dec 2003 15:59:54 +0000 (15:59 +0000)]
- fixed logging in log window so that spurious html tags are no longer
  printed
- factorized a lot of error handling code in invokeTactics
- moved (and reimplemented) logger class to ui_logger module

20 years agorenamed module "logger" to "cicLogger" to avoid confusion with user
Stefano Zacchiroli [Tue, 16 Dec 2003 15:58:38 +0000 (15:58 +0000)]
renamed module "logger" to "cicLogger" to avoid confusion with user
interface logger

20 years agosample script.sh which read META files from ocaml/METAS
Stefano Zacchiroli [Tue, 16 Dec 2003 13:50:41 +0000 (13:50 +0000)]
sample script.sh which read META files from ocaml/METAS

20 years agomoved META files in METAS/ dir
Stefano Zacchiroli [Tue, 16 Dec 2003 13:49:09 +0000 (13:49 +0000)]
moved META files in METAS/ dir

20 years agoadded support for cic_textual_parser2 module
Stefano Zacchiroli [Tue, 16 Dec 2003 08:55:00 +0000 (08:55 +0000)]
added support for cic_textual_parser2 module

20 years agonew experimental cic textual parser: checkin
Stefano Zacchiroli [Mon, 15 Dec 2003 23:00:39 +0000 (23:00 +0000)]
new experimental cic textual parser: checkin

20 years agoclose RC bug regarding rebuilding with newer gthmathview
Stefano Zacchiroli [Wed, 10 Dec 2003 16:57:54 +0000 (16:57 +0000)]
close RC bug regarding rebuilding with newer gthmathview

20 years agomathql documentation for version 4
Ferruccio Guidi [Mon, 8 Dec 2003 16:22:24 +0000 (16:22 +0000)]
mathql documentation for version 4

20 years agodebian version 0.0.4-3
Stefano Zacchiroli [Thu, 4 Dec 2003 16:58:39 +0000 (16:58 +0000)]
debian version 0.0.4-3

20 years agoadded -thread option where needed to make new findlib happy
Stefano Zacchiroli [Thu, 4 Dec 2003 16:58:06 +0000 (16:58 +0000)]
added -thread option where needed to make new findlib happy

20 years agoignore environments
Stefano Zacchiroli [Thu, 4 Dec 2003 16:57:50 +0000 (16:57 +0000)]
ignore environments

20 years agoesplicitely add -thread parameter to all compiler invocations
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:48 +0000 (14:47 +0000)]
esplicitely add -thread parameter to all compiler invocations

20 years agouse a list of getter maps
Stefano Zacchiroli [Wed, 3 Dec 2003 14:47:28 +0000 (14:47 +0000)]
use a list of getter maps