]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Wed, 20 Nov 2002 11:02:32 +0000 (11:02 +0000)]
mqint patched (compilation warning removed)
Andrea Asperti [Wed, 20 Nov 2002 10:52:24 +0000 (10:52 +0000)]
Minor bug fixes:
- forward_{rel|sort}.rdf ==> forward_{rel|sort}.xml
- forward_{rel|sort}.xml were not valid XML documents
Stefano Zacchiroli [Wed, 20 Nov 2002 10:05:27 +0000 (10:05 +0000)]
- added a lot of debugging messages
- changed semantics:
- overflow check is now before already_in check
- old uris are not forgotten
natile [Tue, 19 Nov 2002 17:43:41 +0000 (17:43 +0000)]
Now Pattern module really exists in repository.
natile [Tue, 19 Nov 2002 17:41:36 +0000 (17:41 +0000)]
Pattern module added.
Stefano Zacchiroli [Tue, 19 Nov 2002 16:05:25 +0000 (16:05 +0000)]
added ocaml version of draw_graph and uri_set_queue
Andrea Asperti [Tue, 19 Nov 2002 15:47:20 +0000 (15:47 +0000)]
New metadata for sort and rel.
New metadata schemas.
natile [Mon, 18 Nov 2002 18:06:58 +0000 (18:06 +0000)]
Relation: inverse switch added.
Irene Schena [Mon, 18 Nov 2002 14:49:46 +0000 (14:49 +0000)]
Modified Files:
1) schema-h schema-hth: work in progress schemas
Ferruccio Guidi [Mon, 18 Nov 2002 12:37:50 +0000 (12:37 +0000)]
generator patched for new semantics with structurated attribute names
Ferruccio Guidi [Mon, 18 Nov 2002 12:34:51 +0000 (12:34 +0000)]
structurated attribute names added
Stefano Zacchiroli [Sun, 17 Nov 2002 16:45:29 +0000 (16:45 +0000)]
bumped version to 0.0.3
Stefano Zacchiroli [Sun, 17 Nov 2002 16:19:07 +0000 (16:19 +0000)]
renamed tcp_server module in http_tcp_server to avoid future
name clashes
Stefano Zacchiroli [Sun, 17 Nov 2002 16:16:32 +0000 (16:16 +0000)]
bug fix: reset timeout after processing request in Tcp_server.simple
Stefano Zacchiroli [Sun, 17 Nov 2002 16:15:56 +0000 (16:15 +0000)]
*** empty log message ***
Stefano Zacchiroli [Sun, 17 Nov 2002 16:15:01 +0000 (16:15 +0000)]
Added debug flag and debug_print function
Stefano Zacchiroli [Sun, 17 Nov 2002 16:14:34 +0000 (16:14 +0000)]
.cvsignore for examples dir
Stefano Zacchiroli [Sun, 17 Nov 2002 15:48:37 +0000 (15:48 +0000)]
- split http_parser module (all code that parse http requests and
responses)
- split tcp_server module (which contains different [actually 2]
implementation of Unix.establish_server like functions)
- implemented a tcp_server which doesn't fork
- added ~fork parameter to Http_daemon.start* functions
Stefano Zacchiroli [Fri, 15 Nov 2002 15:06:33 +0000 (15:06 +0000)]
oopss, I forgot to commit .depend last time ...
Stefano Zacchiroli [Fri, 15 Nov 2002 13:17:22 +0000 (13:17 +0000)]
backported new pxp module from branch V7_3_new_exportation
Close an incredible bug (Neturl.Malformed_URL) in fully ocaml proof checker.
Ferruccio Guidi [Thu, 14 Nov 2002 18:02:19 +0000 (18:02 +0000)]
replaced fun with inverse attribute
Ferruccio Guidi [Thu, 14 Nov 2002 17:59:46 +0000 (17:59 +0000)]
added inverse switch for relation and attribute
removed fun
Stefano Zacchiroli [Thu, 14 Nov 2002 17:40:54 +0000 (17:40 +0000)]
name fix due to changes in libhttp-ocaml (e.g. s/Http\.Daemon/Http_daemon/)
natile [Thu, 14 Nov 2002 14:50:40 +0000 (14:50 +0000)]
Attribute files added.
natile [Thu, 14 Nov 2002 14:47:06 +0000 (14:47 +0000)]
Unused files removed.
Stefano Zacchiroli [Thu, 14 Nov 2002 12:00:35 +0000 (12:00 +0000)]
load http.cma instead of http.cmo
Stefano Zacchiroli [Thu, 14 Nov 2002 11:57:58 +0000 (11:57 +0000)]
no longer use -pack and Http.*, now interface is the usual Http_*
Stefano Zacchiroli [Thu, 14 Nov 2002 11:36:36 +0000 (11:36 +0000)]
Now use cm{,x}a
Stefano Zacchiroli [Thu, 14 Nov 2002 11:35:46 +0000 (11:35 +0000)]
Changed source-package name to "ocaml-http"
natile [Wed, 13 Nov 2002 18:55:57 +0000 (18:55 +0000)]
Attribute patched: now takes an extra argument of type bool.
natile [Wed, 13 Nov 2002 18:54:59 +0000 (18:54 +0000)]
Attribute patched with inverse function.
Stefano Zacchiroli [Wed, 13 Nov 2002 14:55:55 +0000 (14:55 +0000)]
switched to OCaml HTTP module
Stefano Zacchiroli [Wed, 13 Nov 2002 14:14:14 +0000 (14:14 +0000)]
added ocaml-http 0.0.1
Claudio Sacerdoti Coen [Tue, 5 Nov 2002 16:21:16 +0000 (16:21 +0000)]
first commit
natile [Mon, 4 Nov 2002 19:05:52 +0000 (19:05 +0000)]
Fun patched.
Enrico Tassi [Mon, 4 Nov 2002 09:26:10 +0000 (09:26 +0000)]
bug found:
- >= is splitted in > or = ,so unification fails
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 16:56:25 +0000 (16:56 +0000)]
...
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 16:55:55 +0000 (16:55 +0000)]
Comments removed.
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 16:55:45 +0000 (16:55 +0000)]
Quotes problem fixed.
Ferruccio Guidi [Thu, 31 Oct 2002 14:24:15 +0000 (14:24 +0000)]
MQueryGenerator ported to use fun "objectName"
topLevel typechecker output was removed
Ferruccio Guidi [Thu, 31 Oct 2002 14:18:37 +0000 (14:18 +0000)]
silly debug output removed from stdout
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 10:20:33 +0000 (10:20 +0000)]
New version of the library added.
Claudio Sacerdoti Coen [Tue, 29 Oct 2002 13:16:41 +0000 (13:16 +0000)]
xmlns:h namespace "fixed"
Claudio Sacerdoti Coen [Tue, 29 Oct 2002 12:32:44 +0000 (12:32 +0000)]
New version for the new DTD.
natile [Mon, 28 Oct 2002 10:36:40 +0000 (10:36 +0000)]
Fun patched but works only in one direction (from the alias to the uri).
Claudio Sacerdoti Coen [Fri, 25 Oct 2002 15:47:55 +0000 (15:47 +0000)]
proof-checker ported to the mowgli version
Claudio Sacerdoti Coen [Fri, 25 Oct 2002 15:47:36 +0000 (15:47 +0000)]
Proof-checker ported to the mowgli version.
Claudio Sacerdoti Coen [Fri, 25 Oct 2002 15:20:07 +0000 (15:20 +0000)]
Better configuration management.
Enrico Tassi [Fri, 25 Oct 2002 08:27:21 +0000 (08:27 +0000)]
Now esempi/fourier.cic end with a proof!
- used change_tac to change from a->False to ~a just before tac2.
Fix: Ad hoc change_tac may not work sometimes. check what Cic.Anonimous means.
Claudio Sacerdoti Coen [Thu, 24 Oct 2002 12:56:36 +0000 (12:56 +0000)]
Bug fixed: I don't know what the bug was exactly, but it happened that
the connection was not closed when using some HTTP 1.1 clients (e.g. wget)
Ferruccio Guidi [Tue, 22 Oct 2002 11:20:08 +0000 (11:20 +0000)]
mqint.ml patched
Ferruccio Guidi [Tue, 22 Oct 2002 11:16:56 +0000 (11:16 +0000)]
topLevel updated to use mqint set_database and get_database
Claudio Sacerdoti Coen [Tue, 22 Oct 2002 09:59:49 +0000 (09:59 +0000)]
Bug ``fixed'': we do not need to apply sym_eqT since the goal we produce
is already 1^-1 = 1 (while Coq produces 1 = 1^-1).
Claudio Sacerdoti Coen [Tue, 22 Oct 2002 08:51:51 +0000 (08:51 +0000)]
- matql_interpreter_galax branch removed once and for ever
- added the dependency to natile-galax. You need to add
/projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib
to your OCAMLPATH to make it compile again.
natile [Tue, 22 Oct 2002 08:45:57 +0000 (08:45 +0000)]
Switching interpreter patched, addedd:
postgres_db
galax_db
get_database
Claudio Sacerdoti Coen [Tue, 22 Oct 2002 08:30:06 +0000 (08:30 +0000)]
The two interpreters are now both in mathql_interpreter. The one actually
used can be choosed setting a global reference.
Claudio Sacerdoti Coen [Mon, 21 Oct 2002 17:09:59 +0000 (17:09 +0000)]
No more useful
natile [Mon, 21 Oct 2002 16:58:37 +0000 (16:58 +0000)]
Old modules (use.ml/mli, eval.ml/mli,...) eliminated.
natile [Mon, 21 Oct 2002 16:54:47 +0000 (16:54 +0000)]
Switching interpreter.
Michele Galatà [Mon, 21 Oct 2002 14:15:10 +0000 (14:15 +0000)]
Comments reindented.
natile [Mon, 21 Oct 2002 13:48:24 +0000 (13:48 +0000)]
Merge of the new_mathql branch with the main branch:
- new query language
- new interpreter for the new query language
NOTE: the galax version of the interpreted is not ported yet (and does not compile)
natile [Mon, 21 Oct 2002 13:42:42 +0000 (13:42 +0000)]
Merge of the new_mathql branch with the main branch:
- new query language implemented
- the locate query is now bug-free (and a _LOT_ faster)
Enrico Tassi [Thu, 17 Oct 2002 16:58:31 +0000 (16:58 +0000)]
- indentation is now in pseudo-functional style!
Enrico Tassi [Thu, 17 Oct 2002 15:16:44 +0000 (15:16 +0000)]
- rewritesimpl_tac added in fourierR.ml (wrong location)
- simpl_tac added in fourierR.ml (wrong location)
- "RewriteSimpl ->" button added
- "Rewrite ->" button removed
Claudio Sacerdoti Coen [Wed, 16 Oct 2002 14:21:06 +0000 (14:21 +0000)]
- write_tac fixed (the list of new goals was empty)
- some new bugs introduced here and there ;-)
Claudio Sacerdoti Coen [Mon, 14 Oct 2002 11:45:32 +0000 (11:45 +0000)]
A tough test for rewrite.
Claudio Sacerdoti Coen [Mon, 14 Oct 2002 11:44:07 +0000 (11:44 +0000)]
- bug fixed: some liftings were missing in the implementation of rewrite
- new feature: rewrite now works up to alpha-equivalence
Claudio Sacerdoti Coen [Fri, 11 Oct 2002 17:58:37 +0000 (17:58 +0000)]
- rewrite extended to handle rewritings with eqT
- equality_replace implemented (based on the new rewriting tactic)
Claudio Sacerdoti Coen [Fri, 11 Oct 2002 17:57:37 +0000 (17:57 +0000)]
Trivial bug in equality_replace fixed: an exception was raised in spite of
returning false.
Claudio Sacerdoti Coen [Fri, 11 Oct 2002 16:47:37 +0000 (16:47 +0000)]
New tactic rewrite implemented.
Not tested yet.
Claudio Sacerdoti Coen [Fri, 11 Oct 2002 15:24:56 +0000 (15:24 +0000)]
- idtac used for debugging removed
- bug fixed: the natural number 1 was mapped to (Rplus R1 R0).
It is now mapped to R1 (as it should be). This close all the
residual bugs.
Still to do: we need to close the last open branch using equality_replace,
as soon as it is implemented.
Enrico Tassi [Fri, 11 Oct 2002 09:38:46 +0000 (09:38 +0000)]
More debug printings.
Replacing the wrong tac with id_tac it goes straight to the end,
lefting 1 more goals open:
0 < (1+0)/(1+0)
Remember that the tactic fails applying
0<1 to 0<1+0
natile [Fri, 11 Oct 2002 07:40:54 +0000 (07:40 +0000)]
Use patched.
Enrico Tassi [Thu, 10 Oct 2002 19:44:25 +0000 (19:44 +0000)]
Added an example to test fourier_tac.
Enrico Tassi [Thu, 10 Oct 2002 19:40:37 +0000 (19:40 +0000)]
Debug printing update, now the unification bug
seems to be in tac_zero_inf_pos.
We get '0 < 1 + 0' instead of '0 < 1'.
Claudio Sacerdoti Coen [Thu, 10 Oct 2002 15:48:33 +0000 (15:48 +0000)]
Handling of the splitting of constants into body + type.
Claudio Sacerdoti Coen [Thu, 10 Oct 2002 15:46:08 +0000 (15:46 +0000)]
Handling of the splitting of constants in body + type.
Claudio Sacerdoti Coen [Thu, 10 Oct 2002 14:11:22 +0000 (14:11 +0000)]
HTTP_GETTER_PORT environment variable added
Claudio Sacerdoti Coen [Wed, 9 Oct 2002 17:28:02 +0000 (17:28 +0000)]
Several bug-fixes:
- apply_tac and my_cut used to generate a new metavariable without
updating the metasenv
- a boolean "false" was used in place of the propositional "False"
- minor fixes
The equality_replace tactic is completely wrong. For now the whole
proof branch that needs it is commented out.
Open bugs:
Some unification problem in the proof that the linear combination can
be derived from the initial disequations.
Claudio Sacerdoti Coen [Wed, 9 Oct 2002 15:09:45 +0000 (15:09 +0000)]
Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.
Claudio Sacerdoti Coen [Wed, 9 Oct 2002 14:48:17 +0000 (14:48 +0000)]
added bootmisc and tomcat scripts
Stefano Zacchiroli [Wed, 9 Oct 2002 12:19:42 +0000 (12:19 +0000)]
added support for unload and reload of predefined stylesheets
Stefano Zacchiroli [Wed, 9 Oct 2002 11:25:16 +0000 (11:25 +0000)]
script that loads predefined uwobo stylesheets
Stefano Zacchiroli [Wed, 9 Oct 2002 09:36:49 +0000 (09:36 +0000)]
added /etc/init.d/ stuff
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:42:42 +0000 (09:42 +0000)]
Web-services ordered by port number.
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:37:47 +0000 (09:37 +0000)]
DRAW_GRAPH_PORT environment variable added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:34:20 +0000 (09:34 +0000)]
URI_SET_QUEUE_PORT and DRAW_GRAPH_PORT added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:33:09 +0000 (09:33 +0000)]
Default ports changed.
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:23:03 +0000 (09:23 +0000)]
URI_SET_QUEUE_PORT environment variable added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:14:29 +0000 (09:14 +0000)]
proofcheckerURL configuration parameter added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:13:53 +0000 (09:13 +0000)]
proofcheckerURL param added
Enrico Tassi [Mon, 7 Oct 2002 20:40:43 +0000 (20:40 +0000)]
fourier_tac without useless recursion
Claudio Sacerdoti Coen [Mon, 7 Oct 2002 16:56:10 +0000 (16:56 +0000)]
- The Getter and UWOBO moved to mowgli.
- The UWOBO default port changed to 8081.
- The Getter default port changed to 48081.
Claudio Sacerdoti Coen [Mon, 7 Oct 2002 16:35:22 +0000 (16:35 +0000)]
- New environment variables set.
- Configuration files for V7_mowgli now also generated.
Enrico Tassi [Mon, 7 Oct 2002 16:30:17 +0000 (16:30 +0000)]
hopefully last tactic update cvs log
Claudio Sacerdoti Coen [Mon, 7 Oct 2002 16:25:55 +0000 (16:25 +0000)]
Initial revision
Claudio Sacerdoti Coen [Mon, 7 Oct 2002 16:11:02 +0000 (16:11 +0000)]
HTTP_GETTER_DTD_BASE_DIR configuration parameter added
Enrico Tassi [Wed, 2 Oct 2002 17:08:50 +0000 (17:08 +0000)]
tactic update
Irene Schena [Wed, 2 Oct 2002 12:08:27 +0000 (12:08 +0000)]
Modified Files:
1) grammar.txt: added parentesis to string-set
Claudio Sacerdoti Coen [Fri, 27 Sep 2002 16:59:23 +0000 (16:59 +0000)]
Better handling of queries. Now both the locate and backward queries give
the user the possibility to disambiguate the answer, and write it in the
input window. Some bugs in the disambiguation process have been fixed.
Finally the output of the query process in the outputhtml window is now
much more verbose.