]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 years agoThis commit was manufactured by cvs2svn to create tag 'premoogle'. premoogle
no author [Tue, 25 May 2004 17:56:07 +0000 (17:56 +0000)]
This commit was manufactured by cvs2svn to create tag 'premoogle'.

20 years ago###############################################################
Luca Padovani [Tue, 25 May 2004 17:56:07 +0000 (17:56 +0000)]
###############################################################
### Partial major upgrade of the HELM/MoWGLI Web interface. ###
###############################################################

WARNING: requires the new UWOBO profiles.

Known bugs:

 1. the JSMmenu for graphs is broken
 2. the configuration stuff is utterly broken: you should rely on
    the default configuration
 3. only HTML has been tested (MathML and ProofTrees are broken for
    sure)
 4. dead code everywhere (e.g. almost all the existent
    javascript code; several tokens in links_library.xsl)

20 years agoNew: UWOBO profiles added.
Luca Padovani [Tue, 25 May 2004 17:54:03 +0000 (17:54 +0000)]
New: UWOBO profiles added.

20 years agowritten a new sort function to postpone the resolution of some types of the goals
Matteo Selmi [Tue, 25 May 2004 07:07:19 +0000 (07:07 +0000)]
written a new sort function to postpone the resolution of some types of the goals

20 years agodon't remove documentation on "make dist" so that documentation will be
Stefano Zacchiroli [Mon, 24 May 2004 12:53:22 +0000 (12:53 +0000)]
don't remove documentation on "make dist" so that documentation will be
part of the generated tarball

20 years ago* setprofileparam ==> setparam
Luca Padovani [Mon, 24 May 2004 12:49:58 +0000 (12:49 +0000)]
* setprofileparam ==> setparam
* serialization/deserialization of the profile file implemented (write-through
  semantics)
* cloning of a profile fixed

20 years agoadded hostname resolution entry
Stefano Zacchiroli [Mon, 24 May 2004 12:47:36 +0000 (12:47 +0000)]
added hostname resolution entry

20 years agoimplemented hostname resolution for "addr" parameter
Stefano Zacchiroli [Mon, 24 May 2004 12:46:57 +0000 (12:46 +0000)]
implemented hostname resolution for "addr" parameter

20 years agorewritten "start" comment, now is almost decent
Stefano Zacchiroli [Mon, 24 May 2004 12:46:40 +0000 (12:46 +0000)]
rewritten "start" comment, now is almost decent

20 years agoemptied implementing all items
Stefano Zacchiroli [Mon, 24 May 2004 12:46:24 +0000 (12:46 +0000)]
emptied implementing all items

20 years agoremoved spurious messages
Stefano Zacchiroli [Mon, 24 May 2004 12:46:15 +0000 (12:46 +0000)]
removed spurious messages

20 years ago- ported to latest API
Stefano Zacchiroli [Mon, 24 May 2004 12:45:56 +0000 (12:45 +0000)]
- ported to latest API
- bumped copyright info

20 years ago- added basic_auth.ml example
Stefano Zacchiroli [Mon, 24 May 2004 12:45:33 +0000 (12:45 +0000)]
- added basic_auth.ml example
- restyled examples list

20 years agodebian snapshot (towards a release)
Stefano Zacchiroli [Mon, 24 May 2004 12:22:17 +0000 (12:22 +0000)]
debian snapshot (towards a release)

20 years agoadded OO interface
Stefano Zacchiroli [Mon, 24 May 2004 12:15:09 +0000 (12:15 +0000)]
added OO interface

20 years ago* preliminary version of profile management
Luca Padovani [Sat, 22 May 2004 07:01:09 +0000 (07:01 +0000)]
* preliminary version of profile management

20 years ago* updated respond_error messages after API change in ocaml-http 0.0.9
Luca Padovani [Sat, 22 May 2004 07:00:06 +0000 (07:00 +0000)]
* updated respond_error messages after API change in ocaml-http 0.0.9

20 years agoAdded a sort function to decide the order of theorems to try in the tactic "auto".
Matteo Selmi [Fri, 21 May 2004 16:44:53 +0000 (16:44 +0000)]
Added a sort function to decide the order of theorems to try in the tactic "auto".

20 years agoadded file locking while writing configuration to file (save_to)
Stefano Zacchiroli [Thu, 20 May 2004 17:17:24 +0000 (17:17 +0000)]
added file locking while writing configuration to file (save_to)

20 years agoopen Helm_registry per default
Stefano Zacchiroli [Thu, 20 May 2004 17:16:56 +0000 (17:16 +0000)]
open Helm_registry per default

20 years agobumped copyright years
Stefano Zacchiroli [Thu, 20 May 2004 16:55:11 +0000 (16:55 +0000)]
bumped copyright years

20 years agoChanged mapping keys <-> environment variables, mixed case envvars are
Stefano Zacchiroli [Thu, 20 May 2004 16:30:32 +0000 (16:30 +0000)]
Changed mapping keys <-> environment variables, mixed case envvars are
now used.

20 years agoported to latest ocaml-http API
Stefano Zacchiroli [Thu, 20 May 2004 16:20:21 +0000 (16:20 +0000)]
ported to latest ocaml-http API

20 years agoported to latest ocaml-http API
Stefano Zacchiroli [Thu, 20 May 2004 16:12:44 +0000 (16:12 +0000)]
ported to latest ocaml-http API

20 years agoreverted code parameter on respond function to its original optionality
Stefano Zacchiroli [Thu, 20 May 2004 16:02:25 +0000 (16:02 +0000)]
reverted code parameter on respond function to its original optionality

20 years agorebuilt
Stefano Zacchiroli [Thu, 20 May 2004 16:02:02 +0000 (16:02 +0000)]
rebuilt

20 years agoported to latest ocaml-http API
Stefano Zacchiroli [Thu, 20 May 2004 15:50:19 +0000 (15:50 +0000)]
ported to latest ocaml-http API

20 years agowritten entry for 0.0.9
Stefano Zacchiroli [Thu, 20 May 2004 15:45:21 +0000 (15:45 +0000)]
written entry for 0.0.9

20 years agorestyled API so that respond_* are statically typechecked
Stefano Zacchiroli [Thu, 20 May 2004 15:45:08 +0000 (15:45 +0000)]
restyled API so that respond_* are statically typechecked

20 years ago- changed API so that respond_* are statically type checked for correct
Stefano Zacchiroli [Thu, 20 May 2004 15:44:43 +0000 (15:44 +0000)]
- changed API so that respond_* are statically type checked for correct
  parameter instantiation
- restyled a lot of code

20 years agoadded support for HEAD requests
Stefano Zacchiroli [Thu, 20 May 2004 15:44:01 +0000 (15:44 +0000)]
added support for HEAD requests

20 years agohttp basic authentication example
Stefano Zacchiroli [Thu, 20 May 2004 14:33:20 +0000 (14:33 +0000)]
http basic authentication example

20 years agoadded support for HTTP (Basic) authentication
Stefano Zacchiroli [Thu, 20 May 2004 14:30:48 +0000 (14:30 +0000)]
added support for HTTP (Basic) authentication

20 years ago- added support for HTTP (Basic) authentication
Stefano Zacchiroli [Thu, 20 May 2004 14:30:27 +0000 (14:30 +0000)]
- added support for HTTP (Basic) authentication
- simplified usage of some internal optional parameters

20 years ago* hbugs moved in ocaml
Luca Padovani [Thu, 20 May 2004 12:10:18 +0000 (12:10 +0000)]
* hbugs moved in ocaml

20 years agoadded some nested sections in order to test "ls" method
Stefano Zacchiroli [Thu, 20 May 2004 12:08:08 +0000 (12:08 +0000)]
added some nested sections in order to test "ls" method

20 years ago- added "has" method
Stefano Zacchiroli [Thu, 20 May 2004 12:07:37 +0000 (12:07 +0000)]
- added "has" method
- added "ls" method
- added "?prefix" parameter to "fold", "iter" and "to_list" methods

20 years agoadded helm-pxp, now needed
Stefano Zacchiroli [Thu, 20 May 2004 12:06:35 +0000 (12:06 +0000)]
added helm-pxp, now needed

20 years agoexpanded content of old topfind
Stefano Zacchiroli [Thu, 20 May 2004 09:39:04 +0000 (09:39 +0000)]
expanded content of old topfind

20 years agono longer needed
Stefano Zacchiroli [Thu, 20 May 2004 09:32:28 +0000 (09:32 +0000)]
no longer needed

20 years agoadded iterators over registry contents (fold, iter, to_list)
Stefano Zacchiroli [Thu, 20 May 2004 09:27:06 +0000 (09:27 +0000)]
added iterators over registry contents (fold, iter, to_list)

20 years agoTempative version: every link is now opened in a new window.
Claudio Sacerdoti Coen [Wed, 19 May 2004 15:51:16 +0000 (15:51 +0000)]
Tempative version: every link is now opened in a new window.
The user is responsible for organizing them.

20 years agoBug fixed: middle-clicking over links in the listing frames should now
Claudio Sacerdoti Coen [Wed, 19 May 2004 15:45:15 +0000 (15:45 +0000)]
Bug fixed: middle-clicking over links in the listing frames should now
work on any browser.

20 years agoTempative version: every link is now opened in a new window.
Claudio Sacerdoti Coen [Wed, 19 May 2004 15:44:37 +0000 (15:44 +0000)]
Tempative version: every link is now opened in a new window.
The user is responsible for organizing them.

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