]>
matita.cs.unibo.it Git - helm.git/log
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 18:42:08 +0000 (18:42 +0000)]
rdf:parseType="Resource" added to backPointer
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 17:48:03 +0000 (17:48 +0000)]
* New metadata for refSort and refRel
* New metadata schema
Stefano Zacchiroli [Wed, 20 Nov 2002 16:56:12 +0000 (16:56 +0000)]
TODO list
Stefano Zacchiroli [Wed, 20 Nov 2002 16:34:22 +0000 (16:34 +0000)]
- changed invoked daemons for proof checker, draw graph and uri set
queue to ocaml ones
- bugfix: use different pid files for old a new libraries daemons
Stefano Zacchiroli [Wed, 20 Nov 2002 16:32:26 +0000 (16:32 +0000)]
added env var DRAW_GRAPH_DIR
Stefano Zacchiroli [Wed, 20 Nov 2002 16:30:18 +0000 (16:30 +0000)]
- get working directory from env var DRAW_GRAPH_DIR
- in case of make failure (which in turn usually depends on uwobo's
failure) return an error message in HTML format
- bugfix: return html file instead of ... nothing :)
- bugfix: print real current directory
Stefano Zacchiroli [Wed, 20 Nov 2002 16:28:03 +0000 (16:28 +0000)]
- http debugging value copied from daemon debugging value
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 16:05:42 +0000 (16:05 +0000)]
<h:depth> must precede <h:occurrence> (to make metadata inversion easier)
Stefano Zacchiroli [Wed, 20 Nov 2002 14:05:19 +0000 (14:05 +0000)]
bumped version to 0.0.4
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 14:04:06 +0000 (14:04 +0000)]
Debug code removed.
Stefano Zacchiroli [Wed, 20 Nov 2002 13:58:22 +0000 (13:58 +0000)]
- bugfix: perform GET parameter parsing on HTTP encoded urls _then_
decode them
- removed now useless pair_of_2_sized_list
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