]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years agomqint patched (compilation warning removed)
Ferruccio Guidi [Wed, 20 Nov 2002 11:02:32 +0000 (11:02 +0000)]
mqint patched (compilation warning removed)

21 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

21 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

21 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.

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

21 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

21 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.

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

21 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

21 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

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

21 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

21 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

21 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

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

21 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

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

21 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.

22 years agoAdded an example to test fourier_tac.
Enrico Tassi [Thu, 10 Oct 2002 19:44:25 +0000 (19:44 +0000)]
Added an example to test fourier_tac.

22 years agoDebug printing update, now the unification bug
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'.

22 years agoHandling of the splitting of constants into body + type.
Claudio Sacerdoti Coen [Thu, 10 Oct 2002 15:48:33 +0000 (15:48 +0000)]
Handling of the splitting of constants into body + type.

22 years agoHandling of the splitting of constants in 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.

22 years agoHTTP_GETTER_PORT environment variable added
Claudio Sacerdoti Coen [Thu, 10 Oct 2002 14:11:22 +0000 (14:11 +0000)]
HTTP_GETTER_PORT environment variable added

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

22 years agoPretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.
Claudio Sacerdoti Coen [Wed, 9 Oct 2002 15:09:45 +0000 (15:09 +0000)]
Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.

22 years agoadded bootmisc and tomcat scripts
Claudio Sacerdoti Coen [Wed, 9 Oct 2002 14:48:17 +0000 (14:48 +0000)]
added bootmisc and tomcat scripts

22 years agoadded support for unload and reload of predefined stylesheets
Stefano Zacchiroli [Wed, 9 Oct 2002 12:19:42 +0000 (12:19 +0000)]
added support for unload and reload of predefined stylesheets

22 years agoscript that loads predefined uwobo stylesheets
Stefano Zacchiroli [Wed, 9 Oct 2002 11:25:16 +0000 (11:25 +0000)]
script that loads predefined uwobo stylesheets

22 years agoadded /etc/init.d/ stuff
Stefano Zacchiroli [Wed, 9 Oct 2002 09:36:49 +0000 (09:36 +0000)]
added /etc/init.d/ stuff

22 years agoWeb-services ordered by port number.
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:42:42 +0000 (09:42 +0000)]
Web-services ordered by port number.

22 years agoDRAW_GRAPH_PORT environment variable added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:37:47 +0000 (09:37 +0000)]
DRAW_GRAPH_PORT environment variable added

22 years agoURI_SET_QUEUE_PORT and DRAW_GRAPH_PORT added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:34:20 +0000 (09:34 +0000)]
URI_SET_QUEUE_PORT and DRAW_GRAPH_PORT added

22 years agoDefault ports changed.
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:33:09 +0000 (09:33 +0000)]
Default ports changed.

22 years agoURI_SET_QUEUE_PORT environment variable added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:23:03 +0000 (09:23 +0000)]
URI_SET_QUEUE_PORT environment variable added

22 years agoproofcheckerURL configuration parameter added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:14:29 +0000 (09:14 +0000)]
proofcheckerURL configuration parameter added

22 years agoproofcheckerURL param added
Claudio Sacerdoti Coen [Tue, 8 Oct 2002 09:13:53 +0000 (09:13 +0000)]
proofcheckerURL param added

22 years agofourier_tac without useless recursion
Enrico Tassi [Mon, 7 Oct 2002 20:40:43 +0000 (20:40 +0000)]
fourier_tac without useless recursion

22 years ago- The Getter and UWOBO moved to mowgli.
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.

22 years ago- New environment variables set.
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.

22 years agohopefully last tactic update cvs log
Enrico Tassi [Mon, 7 Oct 2002 16:30:17 +0000 (16:30 +0000)]
hopefully last tactic update cvs log

22 years agoInitial revision
Claudio Sacerdoti Coen [Mon, 7 Oct 2002 16:25:55 +0000 (16:25 +0000)]
Initial revision

22 years agoHTTP_GETTER_DTD_BASE_DIR configuration parameter added
Claudio Sacerdoti Coen [Mon, 7 Oct 2002 16:11:02 +0000 (16:11 +0000)]
HTTP_GETTER_DTD_BASE_DIR configuration parameter added

22 years agotactic update
Enrico Tassi [Wed, 2 Oct 2002 17:08:50 +0000 (17:08 +0000)]
tactic update

22 years agoModified Files:
Irene Schena [Wed, 2 Oct 2002 12:08:27 +0000 (12:08 +0000)]
Modified Files:
1) grammar.txt: added parentesis to string-set

22 years agoBetter handling of queries. Now both the locate and backward queries give
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.