]> matita.cs.unibo.it Git - helm.git/log
helm.git
22 years ago- added ocamldoc documentation in debian package
Stefano Zacchiroli [Fri, 22 Nov 2002 10:48:34 +0000 (10:48 +0000)]
- added ocamldoc documentation in debian package

22 years ago- fixed wrong @raise ocamldoc tags
Stefano Zacchiroli [Fri, 22 Nov 2002 10:48:03 +0000 (10:48 +0000)]
- fixed wrong @raise ocamldoc tags

22 years ago- added targets relative to ocamldoc doc generation
Stefano Zacchiroli [Fri, 22 Nov 2002 10:47:44 +0000 (10:47 +0000)]
- added targets relative to ocamldoc doc generation

22 years ago- bumped version to 0.0.5
Stefano Zacchiroli [Fri, 22 Nov 2002 10:30:11 +0000 (10:30 +0000)]
- bumped version to 0.0.5

22 years ago- removed old entries from TODO
Stefano Zacchiroli [Fri, 22 Nov 2002 10:27:31 +0000 (10:27 +0000)]
- removed old entries from TODO
- updated changelog

22 years ago- added support for multithreaded daemons
Stefano Zacchiroli [Fri, 22 Nov 2002 10:25:51 +0000 (10:25 +0000)]
- added support for multithreaded daemons
- added a generic 'respond' function, used also as low level for other
  respond functions
- added support for chdir in a given document root before starting
- added toString method to response objects

22 years ago...
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 18:26:47 +0000 (18:26 +0000)]
...

22 years agoFirst version of the stuff to create the DB.
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 18:02:29 +0000 (18:02 +0000)]
First version of the stuff to create the DB.

22 years agoThe notational stylesheets from CIC to MathML Content are now automatically
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 17:00:49 +0000 (17:00 +0000)]
The notational stylesheets from CIC to MathML Content are now automatically
generated by Di Lena's meta_style. Rember to add a new entry to servers.txt!!!

22 years agoFirst version of Di Lena's stylesheet generator (for the HELM DTD).
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 16:58:01 +0000 (16:58 +0000)]
First version of Di Lena's stylesheet generator (for the HELM DTD).

22 years agotypo fixed
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 14:40:37 +0000 (14:40 +0000)]
typo fixed

22 years ago*.yy.c removed
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 14:40:02 +0000 (14:40 +0000)]
*.yy.c removed

22 years ago*.rdf ==> *.xml
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 14:37:36 +0000 (14:37 +0000)]
*.rdf ==> *.xml

22 years ago...
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 13:13:53 +0000 (13:13 +0000)]
...

22 years ago<h:Object> is now repeated every time a MainHypothesis (with its depth) is
Claudio Sacerdoti Coen [Thu, 21 Nov 2002 11:01:24 +0000 (11:01 +0000)]
<h:Object> is now repeated every time a MainHypothesis (with its depth) is
printed. The RDF file gets a bit bigger, but lexical analysing it becomes
much easier.

22 years agoBug fixed: refSort were exported (as refObj) also when occurring InHypothesis
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 18:52:27 +0000 (18:52 +0000)]
Bug fixed: refSort were exported (as refObj) also when occurring InHypothesis
and InConclusion.

22 years agordf:parseType="Resource" added to backPointer
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 18:42:08 +0000 (18:42 +0000)]
rdf:parseType="Resource" added to backPointer

22 years ago* New metadata for refSort and refRel
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 17:48:03 +0000 (17:48 +0000)]
* New metadata for refSort and refRel
* New metadata schema

22 years agoTODO list
Stefano Zacchiroli [Wed, 20 Nov 2002 16:56:12 +0000 (16:56 +0000)]
TODO list

22 years ago- changed invoked daemons for proof checker, draw graph and uri set
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

22 years agoadded env var DRAW_GRAPH_DIR
Stefano Zacchiroli [Wed, 20 Nov 2002 16:32:26 +0000 (16:32 +0000)]
added env var DRAW_GRAPH_DIR

22 years ago- get working directory from 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

22 years ago- http debugging value copied from daemon debugging value
Stefano Zacchiroli [Wed, 20 Nov 2002 16:28:03 +0000 (16:28 +0000)]
- http debugging value copied from daemon debugging value

22 years ago<h:depth> must precede <h:occurrence> (to make metadata inversion easier)
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)

22 years agobumped version to 0.0.4
Stefano Zacchiroli [Wed, 20 Nov 2002 14:05:19 +0000 (14:05 +0000)]
bumped version to 0.0.4

22 years agoDebug code removed.
Claudio Sacerdoti Coen [Wed, 20 Nov 2002 14:04:06 +0000 (14:04 +0000)]
Debug code removed.

22 years ago- bugfix: perform GET parameter parsing on HTTP encoded urls _then_
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

22 years agomqint patched (compilation warning removed)
Ferruccio Guidi [Wed, 20 Nov 2002 11:02:32 +0000 (11:02 +0000)]
mqint patched (compilation warning removed)

22 years agoMinor bug fixes:
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

22 years ago- added a lot of debugging messages
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

22 years agoNow Pattern module really exists in repository.
natile [Tue, 19 Nov 2002 17:43:41 +0000 (17:43 +0000)]
Now Pattern module really exists in repository.

22 years agoPattern module added.
natile [Tue, 19 Nov 2002 17:41:36 +0000 (17:41 +0000)]
Pattern module added.

22 years agoadded ocaml version of draw_graph and uri_set_queue
Stefano Zacchiroli [Tue, 19 Nov 2002 16:05:25 +0000 (16:05 +0000)]
added ocaml version of draw_graph and uri_set_queue

22 years agoNew metadata for sort and rel.
Andrea Asperti [Tue, 19 Nov 2002 15:47:20 +0000 (15:47 +0000)]
New metadata for sort and rel.
New metadata schemas.

22 years agoRelation: inverse switch added.
natile [Mon, 18 Nov 2002 18:06:58 +0000 (18:06 +0000)]
Relation: inverse switch added.

22 years agoModified Files:
Irene Schena [Mon, 18 Nov 2002 14:49:46 +0000 (14:49 +0000)]
Modified Files:
1) schema-h schema-hth: work in progress schemas

22 years agogenerator patched for new semantics with structurated attribute names
Ferruccio Guidi [Mon, 18 Nov 2002 12:37:50 +0000 (12:37 +0000)]
generator patched for new semantics with structurated attribute names

22 years agostructurated attribute names added
Ferruccio Guidi [Mon, 18 Nov 2002 12:34:51 +0000 (12:34 +0000)]
structurated attribute names added

22 years agobumped version to 0.0.3
Stefano Zacchiroli [Sun, 17 Nov 2002 16:45:29 +0000 (16:45 +0000)]
bumped version to 0.0.3

22 years agorenamed tcp_server module in http_tcp_server to avoid future
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

22 years agobug fix: reset timeout after processing request in Tcp_server.simple
Stefano Zacchiroli [Sun, 17 Nov 2002 16:16:32 +0000 (16:16 +0000)]
bug fix: reset timeout after processing request in Tcp_server.simple

22 years ago*** empty log message ***
Stefano Zacchiroli [Sun, 17 Nov 2002 16:15:56 +0000 (16:15 +0000)]
*** empty log message ***

22 years agoAdded debug flag and debug_print function
Stefano Zacchiroli [Sun, 17 Nov 2002 16:15:01 +0000 (16:15 +0000)]
Added debug flag and debug_print function

22 years ago.cvsignore for examples dir
Stefano Zacchiroli [Sun, 17 Nov 2002 16:14:34 +0000 (16:14 +0000)]
.cvsignore for examples dir

22 years ago- split http_parser module (all code that parse http requests and
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

22 years agooopss, I forgot to commit .depend last time ...
Stefano Zacchiroli [Fri, 15 Nov 2002 15:06:33 +0000 (15:06 +0000)]
oopss, I forgot to commit .depend last time ...

22 years agobackported new pxp module from branch V7_3_new_exportation
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.

22 years agoreplaced fun with inverse attribute
Ferruccio Guidi [Thu, 14 Nov 2002 18:02:19 +0000 (18:02 +0000)]
replaced fun with inverse attribute

22 years agoadded inverse switch for relation and attribute
Ferruccio Guidi [Thu, 14 Nov 2002 17:59:46 +0000 (17:59 +0000)]
added inverse switch for relation and attribute
removed fun

22 years agoname fix due to changes in libhttp-ocaml (e.g. s/Http\.Daemon/Http_daemon/)
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/)

22 years agoAttribute files added.
natile [Thu, 14 Nov 2002 14:50:40 +0000 (14:50 +0000)]
Attribute files added.

22 years agoUnused files removed.
natile [Thu, 14 Nov 2002 14:47:06 +0000 (14:47 +0000)]
Unused files removed.

22 years agoload http.cma instead of http.cmo
Stefano Zacchiroli [Thu, 14 Nov 2002 12:00:35 +0000 (12:00 +0000)]
load http.cma instead of http.cmo

22 years agono longer use -pack and Http.*, now interface is the usual Http_*
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_*

22 years agoNow use cm{,x}a
Stefano Zacchiroli [Thu, 14 Nov 2002 11:36:36 +0000 (11:36 +0000)]
Now use cm{,x}a

22 years agoChanged source-package name to "ocaml-http"
Stefano Zacchiroli [Thu, 14 Nov 2002 11:35:46 +0000 (11:35 +0000)]
Changed source-package name to "ocaml-http"

22 years agoAttribute patched: now takes an extra argument of type bool.
natile [Wed, 13 Nov 2002 18:55:57 +0000 (18:55 +0000)]
Attribute patched: now takes an extra argument of type bool.

22 years agoAttribute patched with inverse function.
natile [Wed, 13 Nov 2002 18:54:59 +0000 (18:54 +0000)]
Attribute patched with inverse function.

22 years agoswitched to OCaml HTTP module
Stefano Zacchiroli [Wed, 13 Nov 2002 14:55:55 +0000 (14:55 +0000)]
switched to OCaml HTTP module

22 years agoadded ocaml-http 0.0.1
Stefano Zacchiroli [Wed, 13 Nov 2002 14:14:14 +0000 (14:14 +0000)]
added ocaml-http 0.0.1

22 years agofirst commit
Claudio Sacerdoti Coen [Tue, 5 Nov 2002 16:21:16 +0000 (16:21 +0000)]
first commit

22 years agoFun patched.
natile [Mon, 4 Nov 2002 19:05:52 +0000 (19:05 +0000)]
Fun patched.

22 years agobug found:
Enrico Tassi [Mon, 4 Nov 2002 09:26:10 +0000 (09:26 +0000)]
bug found:
 - >= is splitted in > or = ,so unification fails

22 years ago...
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 16:56:25 +0000 (16:56 +0000)]
...

22 years agoComments removed.
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 16:55:55 +0000 (16:55 +0000)]
Comments removed.

22 years agoQuotes problem fixed.
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 16:55:45 +0000 (16:55 +0000)]
Quotes problem fixed.

22 years agoMQueryGenerator ported to use fun "objectName"
Ferruccio Guidi [Thu, 31 Oct 2002 14:24:15 +0000 (14:24 +0000)]
MQueryGenerator ported to use fun "objectName"
topLevel        typechecker output was removed

22 years agosilly debug output removed from stdout
Ferruccio Guidi [Thu, 31 Oct 2002 14:18:37 +0000 (14:18 +0000)]
silly debug output removed from stdout

22 years agoNew version of the library added.
Claudio Sacerdoti Coen [Thu, 31 Oct 2002 10:20:33 +0000 (10:20 +0000)]
New version of the library added.

22 years agoxmlns:h namespace "fixed"
Claudio Sacerdoti Coen [Tue, 29 Oct 2002 13:16:41 +0000 (13:16 +0000)]
xmlns:h namespace "fixed"

22 years agoNew version for the new DTD.
Claudio Sacerdoti Coen [Tue, 29 Oct 2002 12:32:44 +0000 (12:32 +0000)]
New version for the new DTD.

22 years agoFun patched but works only in one direction (from the alias to the uri).
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).

22 years agoproof-checker ported to the mowgli version
Claudio Sacerdoti Coen [Fri, 25 Oct 2002 15:47:55 +0000 (15:47 +0000)]
proof-checker ported to the mowgli version

22 years agoProof-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.

22 years agoBetter configuration management.
Claudio Sacerdoti Coen [Fri, 25 Oct 2002 15:20:07 +0000 (15:20 +0000)]
Better configuration management.

22 years agoNow esempi/fourier.cic end with a proof!
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.

22 years agoBug fixed: I don't know what the bug was exactly, but it happened that
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)

22 years agomqint.ml patched
Ferruccio Guidi [Tue, 22 Oct 2002 11:20:08 +0000 (11:20 +0000)]
mqint.ml patched

22 years agotopLevel updated to use mqint set_database and get_database
Ferruccio Guidi [Tue, 22 Oct 2002 11:16:56 +0000 (11:16 +0000)]
topLevel updated to use mqint set_database and get_database

22 years agoBug ``fixed'': we do not need to apply sym_eqT since the goal we produce
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).

22 years ago- matql_interpreter_galax branch removed once and for ever
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.

22 years agoSwitching interpreter patched, addedd:
natile [Tue, 22 Oct 2002 08:45:57 +0000 (08:45 +0000)]
Switching interpreter patched, addedd:
 postgres_db
 galax_db
 get_database

22 years agoThe two interpreters are now both in mathql_interpreter. The one actually
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.

22 years agoNo more useful
Claudio Sacerdoti Coen [Mon, 21 Oct 2002 17:09:59 +0000 (17:09 +0000)]
No more useful

22 years agoOld modules (use.ml/mli, eval.ml/mli,...) eliminated.
natile [Mon, 21 Oct 2002 16:58:37 +0000 (16:58 +0000)]
Old modules (use.ml/mli, eval.ml/mli,...) eliminated.

22 years agoSwitching interpreter.
natile [Mon, 21 Oct 2002 16:54:47 +0000 (16:54 +0000)]
Switching interpreter.

22 years agoComments reindented.
Michele Galatà [Mon, 21 Oct 2002 14:15:10 +0000 (14:15 +0000)]
Comments reindented.

22 years agoMerge of the new_mathql branch with the main branch:
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)

22 years agoMerge of the new_mathql branch with the main branch:
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)

22 years ago- indentation is now in pseudo-functional style!
Enrico Tassi [Thu, 17 Oct 2002 16:58:31 +0000 (16:58 +0000)]
- indentation is now in pseudo-functional style!

22 years ago- rewritesimpl_tac added in fourierR.ml (wrong location)
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

22 years ago- write_tac fixed (the list of new goals was empty)
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 ;-)

22 years agoA tough test for rewrite.
Claudio Sacerdoti Coen [Mon, 14 Oct 2002 11:45:32 +0000 (11:45 +0000)]
A tough test for rewrite.

22 years ago- bug fixed: some liftings were missing in the implementation of 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

22 years ago- rewrite extended to handle rewritings with eqT
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)

22 years agoTrivial bug in equality_replace fixed: an exception was raised in spite of
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.

22 years agoNew tactic rewrite implemented.
Claudio Sacerdoti Coen [Fri, 11 Oct 2002 16:47:37 +0000 (16:47 +0000)]
New tactic rewrite implemented.
Not tested yet.

22 years ago- idtac used for debugging removed
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.

22 years agoMore debug printings.
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

22 years agoUse patched.
natile [Fri, 11 Oct 2002 07:40:54 +0000 (07:40 +0000)]
Use patched.