]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agomoogle snapshot moogle
Andrea Asperti [Wed, 19 May 2004 14:41:41 +0000 (14:41 +0000)]
moogle snapshot

20 years agoThis commit was manufactured by cvs2svn to create branch 'moogle'.
no author [Wed, 19 May 2004 14:39:42 +0000 (14:39 +0000)]
This commit was manufactured by cvs2svn to create branch 'moogle'.

20 years agofirst moogle template checkin
Andrea Asperti [Wed, 19 May 2004 14:39:42 +0000 (14:39 +0000)]
first moogle template checkin

20 years ago* the input of the function mkMetaTheoryURL must an (unquoted) URI. Fixed.
Claudio Sacerdoti Coen [Tue, 18 May 2004 17:12:05 +0000 (17:12 +0000)]
* the input of the function mkMetaTheoryURL must an (unquoted) URI. Fixed.

20 years ago* the URI passed to the rdfly deamon is now CICURI, except that quoting
Claudio Sacerdoti Coen [Tue, 18 May 2004 16:06:07 +0000 (16:06 +0000)]
* the URI passed to the rdfly deamon is now CICURI, except that quoting
  rules are different.

20 years ago* [Luca] string concatenation now made using String.concat instead of
Claudio Sacerdoti Coen [Tue, 18 May 2004 15:57:23 +0000 (15:57 +0000)]
* [Luca] string concatenation now made using String.concat instead of
  List.fold_left

20 years agoNuova implementazione di Auto "breadth-first".
Andrea Asperti [Tue, 18 May 2004 13:25:35 +0000 (13:25 +0000)]
Nuova implementazione di Auto "breadth-first".

20 years agoxml:base and helm:base are now generated only for theories.
Claudio Sacerdoti Coen [Tue, 18 May 2004 09:16:31 +0000 (09:16 +0000)]
xml:base and helm:base are now generated only for theories.

20 years ago* tactics/Makefile fixed (to remove duplicate .mli files)
Claudio Sacerdoti Coen [Tue, 18 May 2004 08:56:50 +0000 (08:56 +0000)]
* tactics/Makefile fixed (to remove duplicate .mli files)
* .depend regenerated

20 years agoBug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
Claudio Sacerdoti Coen [Tue, 18 May 2004 08:39:54 +0000 (08:39 +0000)]
Bug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
were full URIs (with also the filename at the end). Fixed by using
Filename.dirname (that seems to work also with generic URIs).

20 years agoAdded a filter for uris in tactic "auto".
Matteo Selmi [Mon, 17 May 2004 20:58:56 +0000 (20:58 +0000)]
Added a filter for uris in tactic "auto".
Uris of theorems containing, in the conclusion or in the hypothesis, constants not present in the proof (hypothesis or conclusion) are filtered out.

20 years agoAdded support for xml base(s) URL and URI. The getter now adds these two
Stefano Zacchiroli [Mon, 17 May 2004 17:48:33 +0000 (17:48 +0000)]
Added support for xml base(s) URL and URI. The getter now adds these two
attributes (hopefully) on the first open tag

20 years agofirst check in of statefulProofEngine
Stefano Zacchiroli [Mon, 17 May 2004 12:30:19 +0000 (12:30 +0000)]
first check in of statefulProofEngine

20 years agobugfix: remove trailing slashes from dtd_base_urls
Stefano Zacchiroli [Mon, 17 May 2004 11:35:37 +0000 (11:35 +0000)]
bugfix: remove trailing slashes from dtd_base_urls

20 years ago- some code patched
Ferruccio Guidi [Thu, 13 May 2004 13:32:12 +0000 (13:32 +0000)]
- some code patched
- mathql documentation updated

20 years agochanged proofStatus so that uri component is optional (useful to start an
Stefano Zacchiroli [Thu, 13 May 2004 12:59:43 +0000 (12:59 +0000)]
changed proofStatus so that uri component is optional (useful to start an
unnamed proof or leave the possibility of postpone uri choice)

20 years ago*** empty log message ***
Andrea Asperti [Mon, 10 May 2004 13:31:57 +0000 (13:31 +0000)]
*** empty log message ***

20 years agoAdding file newConstraint
Andrea Asperti [Mon, 10 May 2004 09:43:55 +0000 (09:43 +0000)]
Adding file newConstraint
The file contains functions for computing prefixes and related
stuff, required by the new management of matching.

20 years agoAdding file match_concl
Andrea Asperti [Mon, 10 May 2004 09:40:33 +0000 (09:40 +0000)]
Adding file match_concl
the file contains:
   - functions executing must, just and only constraints on the mysql
     data base;
   - the general function cmatch for retrieving all statements matching
     a given conclusion

20 years agosnapshot (notably: first working version of the console)
Stefano Zacchiroli [Tue, 4 May 2004 10:47:10 +0000 (10:47 +0000)]
snapshot (notably: first working version of the console)

20 years ago- moved up in the grammar precedences command entry so that sequence of
Stefano Zacchiroli [Tue, 4 May 2004 10:46:39 +0000 (10:46 +0000)]
- moved up in the grammar precedences command entry so that sequence of
  commands are not permitted
- added parsing of "abort" command

20 years agoremoved traliling dot in command pretty printer, now it's added by the
Stefano Zacchiroli [Tue, 4 May 2004 10:45:54 +0000 (10:45 +0000)]
removed traliling dot in command pretty printer, now it's added by the
tactical pp

20 years agoadded Abort and Check commands
Stefano Zacchiroli [Fri, 30 Apr 2004 14:00:15 +0000 (14:00 +0000)]
added Abort and Check commands

20 years agoembedded commands ast into tacticals ast
Stefano Zacchiroli [Fri, 30 Apr 2004 09:25:36 +0000 (09:25 +0000)]
embedded commands ast into tacticals ast

20 years ago- moved command as sub-entries of tactical grammars (as per tactics)
Stefano Zacchiroli [Fri, 30 Apr 2004 09:24:49 +0000 (09:24 +0000)]
- moved command as sub-entries of tactical grammars (as per tactics)

20 years agosnapshot
Stefano Zacchiroli [Fri, 30 Apr 2004 08:23:12 +0000 (08:23 +0000)]
snapshot

20 years ago- moved applyTransformation initialization code to the relevant library
Stefano Zacchiroli [Thu, 29 Apr 2004 16:15:25 +0000 (16:15 +0000)]
- moved applyTransformation initialization code to the relevant library
- decoupled termViewer from ChosenTransformer

20 years agomoved here initialization code (previously in gTopLevel/termViewer.ml)
Stefano Zacchiroli [Thu, 29 Apr 2004 16:14:33 +0000 (16:14 +0000)]
moved here initialization code (previously in gTopLevel/termViewer.ml)

20 years agosnapshot
Stefano Zacchiroli [Thu, 29 Apr 2004 13:59:11 +0000 (13:59 +0000)]
snapshot

20 years ago- added a configuration variable for selecting between fresh instances
Stefano Zacchiroli [Thu, 29 Apr 2004 13:55:31 +0000 (13:55 +0000)]
- added a configuration variable for selecting between fresh instances
  for numbers or not (set by default to a single instance)

20 years agosnapshot
Stefano Zacchiroli [Wed, 28 Apr 2004 20:45:38 +0000 (20:45 +0000)]
snapshot

20 years agoadded a TODO comment
Stefano Zacchiroli [Wed, 28 Apr 2004 20:45:16 +0000 (20:45 +0000)]
added a TODO comment

20 years agorebuilt
Stefano Zacchiroli [Wed, 28 Apr 2004 15:04:31 +0000 (15:04 +0000)]
rebuilt

20 years agoadded extra "id" parameter for input_or_locate_uri callback
Stefano Zacchiroli [Wed, 28 Apr 2004 15:04:11 +0000 (15:04 +0000)]
added extra "id" parameter for input_or_locate_uri callback

20 years ago- split logic operators away from aritmetic ones so that
Stefano Zacchiroli [Wed, 28 Apr 2004 14:11:51 +0000 (14:11 +0000)]
- split logic operators away from aritmetic ones so that
   \forall n:nat. n > 0 \or n = 0
  is parsed "correctly"

20 years agoremoved file:// prefix from local_library key, hopefully it isn't useful
Stefano Zacchiroli [Wed, 28 Apr 2004 14:00:42 +0000 (14:00 +0000)]
removed file:// prefix from local_library key, hopefully it isn't useful

20 years agosnapshot
Stefano Zacchiroli [Fri, 23 Apr 2004 14:54:46 +0000 (14:54 +0000)]
snapshot

20 years agogt URL pointed to lt
Claudio Sacerdoti Coen [Fri, 23 Apr 2004 12:57:29 +0000 (12:57 +0000)]
gt URL pointed to lt

20 years agoUniverses introduction
Enrico Tassi [Fri, 23 Apr 2004 10:37:00 +0000 (10:37 +0000)]
Universes introduction

20 years agordfly hardcoded URL changed from mowgli.cs.unibo.it to localhost
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

20 years agoexpandasking parameter passed to UWOBO.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 17:00:31 +0000 (17:00 +0000)]
expandasking parameter passed to UWOBO.

20 years agosnapshot
Stefano Zacchiroli [Thu, 22 Apr 2004 16:33:02 +0000 (16:33 +0000)]
snapshot

20 years agomysql_connection.* keys added
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 15:02:50 +0000 (15:02 +0000)]
mysql_connection.* keys added

20 years agomathql_interpreter.mysql_connection.* keys added.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 15:00:11 +0000 (15:00 +0000)]
mathql_interpreter.mysql_connection.* keys added.

20 years agoadded (and used) some type shorthands
Stefano Zacchiroli [Thu, 22 Apr 2004 13:54:12 +0000 (13:54 +0000)]
added (and used) some type shorthands

20 years ago- added some type shorthands
Stefano Zacchiroli [Thu, 22 Apr 2004 13:53:49 +0000 (13:53 +0000)]
- added some type shorthands
- added license information

20 years agorebuit
Stefano Zacchiroli [Thu, 22 Apr 2004 13:53:22 +0000 (13:53 +0000)]
rebuit

20 years agoPatches to generate ?1 : ?2 : Type in place of ?1 : Type removed.
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.

20 years agoBig bug fixed: in the case t <?= ?1, the instantiation ?1 := t was generated
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).

20 years agofourier.mli addedto interface files.
Enrico Tassi [Thu, 22 Apr 2004 11:29:14 +0000 (11:29 +0000)]
fourier.mli addedto interface files.

20 years agosnapshot
Stefano Zacchiroli [Thu, 22 Apr 2004 10:41:14 +0000 (10:41 +0000)]
snapshot

20 years agoadded /help method (needed by respawner)
Stefano Zacchiroli [Thu, 22 Apr 2004 09:36:54 +0000 (09:36 +0000)]
added /help method (needed by respawner)

20 years agoIMPLEMENTATION_FILES now generated from INTERFACE_FILES.
Claudio Sacerdoti Coen [Thu, 22 Apr 2004 09:11:16 +0000 (09:11 +0000)]
IMPLEMENTATION_FILES now generated from INTERFACE_FILES.

20 years agoadded .cvsignore
Stefano Zacchiroli [Thu, 22 Apr 2004 08:31:19 +0000 (08:31 +0000)]
added .cvsignore

20 years agodetects and uses {ocamlc,ocamlopt}.opt when available
Stefano Zacchiroli [Wed, 21 Apr 2004 17:46:17 +0000 (17:46 +0000)]
detects and uses {ocamlc,ocamlopt}.opt when available

20 years agodetect and use {ocamlc,ocamlopt}.opt when they are available
Stefano Zacchiroli [Wed, 21 Apr 2004 17:35:00 +0000 (17:35 +0000)]
detect and use {ocamlc,ocamlopt}.opt when they are available

20 years agoexported term_of_uri
Stefano Zacchiroli [Wed, 21 Apr 2004 17:29:35 +0000 (17:29 +0000)]
exported term_of_uri

20 years agoadded helmLibraryObjects.mli mention
Stefano Zacchiroli [Wed, 21 Apr 2004 17:26:39 +0000 (17:26 +0000)]
added helmLibraryObjects.mli mention

20 years agoadded .mli
Stefano Zacchiroli [Wed, 21 Apr 2004 16:36:38 +0000 (16:36 +0000)]
added .mli

20 years agogot rid of a ~status label
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:53 +0000 (17:00 +0000)]
got rid of a ~status label

20 years agogot rid of ~status label
Stefano Zacchiroli [Tue, 20 Apr 2004 17:00:27 +0000 (17:00 +0000)]
got rid of ~status label

20 years agogot rid of ~status label so that tactics can now be applied partially,
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, ...

20 years agoadded ocamlfind library checks to configure.ac
Stefano Zacchiroli [Tue, 20 Apr 2004 09:41:10 +0000 (09:41 +0000)]
added ocamlfind library checks to configure.ac

20 years agorenamed mathita to matita
Stefano Zacchiroli [Tue, 20 Apr 2004 09:27:36 +0000 (09:27 +0000)]
renamed mathita to matita

20 years agosnapshot
Stefano Zacchiroli [Tue, 20 Apr 2004 08:54:23 +0000 (08:54 +0000)]
snapshot

20 years agoignore Makefile since now it's generated by configure
Stefano Zacchiroli [Mon, 19 Apr 2004 12:12:35 +0000 (12:12 +0000)]
ignore Makefile since now it's generated by configure

20 years agoadded Makefile.in
Stefano Zacchiroli [Mon, 19 Apr 2004 12:12:16 +0000 (12:12 +0000)]
added Makefile.in

20 years agoreorganized metas so that pxp is references only through helm-pxp
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:37 +0000 (12:10 +0000)]
reorganized metas so that pxp is references only through helm-pxp

20 years agoadded hbugs' (client) meta
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:20 +0000 (12:10 +0000)]
added hbugs' (client) meta

20 years agogeneralized META.* ignoring
Stefano Zacchiroli [Mon, 19 Apr 2004 12:10:03 +0000 (12:10 +0000)]
generalized META.* ignoring

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