TODO list

- 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

added env var DRAW_GRAPH_DIR

- 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

- http debugging value copied from daemon debugging value

<h:depth> must precede <h:occurrence> (to make metadata inversion easier)

bumped version to 0.0.4

Debug code removed.

- bugfix: perform GET parameter parsing on HTTP encoded urls _then_
  decode them
- removed now useless pair_of_2_sized_list

mqint patched (compilation warning removed)

Minor bug fixes:
 - forward_{rel|sort}.rdf ==> forward_{rel|sort}.xml
 - forward_{rel|sort}.xml were not valid XML documents

- added a lot of debugging messages
- changed semantics:
  - overflow check is now before already_in check
  - old uris are not forgotten

Now Pattern module really exists in repository.

Pattern module added.

added ocaml version of draw_graph and uri_set_queue

New metadata for sort and rel.
New metadata schemas.

Relation: inverse switch added.

Modified Files:
1) schema-h schema-hth: work in progress schemas

generator patched for new semantics with structurated attribute names

structurated attribute names added

bumped version to 0.0.3

renamed tcp_server module in http_tcp_server to avoid future
name clashes

bug fix: reset timeout after processing request in Tcp_server.simple

*** empty log message ***

Added debug flag and debug_print function

.cvsignore for examples dir

- 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

oopss, I forgot to commit .depend last time ...

backported new pxp module from branch V7_3_new_exportation
Close an incredible bug (Neturl.Malformed_URL) in fully ocaml proof checker.

replaced fun with inverse attribute

added inverse switch for relation and attribute
removed fun

name fix due to changes in libhttp-ocaml (e.g. s/Http\.Daemon/Http_daemon/)

Attribute files added.

Unused files removed.

load http.cma instead of http.cmo

no longer use -pack and Http.*, now interface is the usual Http_*

Now use cm{,x}a

Changed source-package name to "ocaml-http"

Attribute patched: now takes an extra argument of type bool.

Attribute patched with inverse function.

switched to OCaml HTTP module

added ocaml-http 0.0.1

first commit

Fun patched.

bug found:
 - >= is splitted in > or = ,so unification fails

...

Comments removed.

Quotes problem fixed.

MQueryGenerator ported to use fun "objectName"
topLevel        typechecker output was removed

silly debug output removed from stdout

New version of the library added.

xmlns:h namespace "fixed"

New version for the new DTD.

Fun patched but works only in one direction (from the alias to the uri).

proof-checker ported to the mowgli version

Proof-checker ported to the mowgli version.

Better configuration management.

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.

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)

mqint.ml patched

topLevel updated to use mqint set_database and get_database

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

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

Switching interpreter patched, addedd:
 postgres_db
 galax_db
 get_database

The two interpreters are now both in mathql_interpreter. The one actually
used can be choosed setting a global reference.

No more useful

Old modules (use.ml/mli, eval.ml/mli,...) eliminated.

Switching interpreter.

Comments reindented.

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)

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)

- indentation is now in pseudo-functional style!

- rewritesimpl_tac added in fourierR.ml (wrong location)
- simpl_tac added in fourierR.ml (wrong location)
- "RewriteSimpl ->" button added
- "Rewrite ->" button removed

- write_tac fixed (the list of new goals was empty)
- some new bugs introduced here and there ;-)

A tough test for rewrite.

- bug fixed: some liftings were missing in the implementation of rewrite
- new feature: rewrite now works up to alpha-equivalence

- rewrite extended to handle rewritings with eqT
- equality_replace implemented (based on the new rewriting tactic)

Trivial bug in equality_replace fixed: an exception was raised in spite of
returning false.

New tactic rewrite implemented.
Not tested yet.

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

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

Use patched.

Added an example to test fourier_tac.

Debug printing update, now the unification bug
seems to be in tac_zero_inf_pos.

We get '0 < 1 + 0' instead of '0 < 1'.

Handling of the splitting of constants into body + type.

Handling of the splitting of constants in body + type.

HTTP_GETTER_PORT environment variable added

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.

Pretty-printing of MUTIND and MUTCONSTRUCT with crazy indexes fixed.

added bootmisc and tomcat scripts

added support for unload and reload of predefined stylesheets

script that loads predefined uwobo stylesheets

added /etc/init.d/ stuff

Web-services ordered by port number.

DRAW_GRAPH_PORT environment variable added

URI_SET_QUEUE_PORT and DRAW_GRAPH_PORT added

Default ports changed.

URI_SET_QUEUE_PORT environment variable added

proofcheckerURL configuration parameter added

proofcheckerURL param added