snapshot

ignore Makefile since now it's generated by configure

added Makefile.in

reorganized metas so that pxp is references only through helm-pxp

added hbugs' (client) meta

generalized META.* ignoring

- reordered modules so that pxp could be used as entry point for pxp
- added hbugs
- pretty printed modules

- use PxpHelmConf
- no longer use deprecated Pxp_yacc module

- use PxpHelmConf
- no longer use deprecated Pxp_yacc

use PxpHelmConf

added dep on Helm_registry

use PxpHelmConf module

- use PxpHelmConf
- removed references to deprecated Pxp_yacc module

- embedded ClientHTTP module (not very nice, but ClientHTTP shouldn't
  belongs to Getter module!)
- added PxpHelmConf module, repository of Pxp configurations for helm

added ExtThread module, ex Hbugs_deity (a Thread module with killing
capabilities)

injected hbugs under ocaml/ dir

moved hbugs under ocaml/

fixed a typo (inside a comment)

test_equality_only was not used in sort comparison.
It should be implemented only in unification.

use respawner

changed logging message

removed deprecated uwobo_forever.sh

removed tedious "_mowgli" postfix

use new daemon_respawner.sh

fixed some typos in sample init.d

added generic daemon respawner

script deprecated

added newline to log when log_file is in use

- addead autoconf-iguration. Actually it only set the default runtime
  configuration file

- use new logger interface
- added support for log_level and log_file in configuration file

- rewritten http_getter logger interface

- added sample usage of get_opt method
- added method get_opt_default (like get_opt with an additional default
  value)

Metasenv added as parameter to eta_fixing.

s/dtd_base_url/dtd_base_urls/

- better pretty printing of exceptions (added red color)
- added "-update" command line parameter for batch updating

- fixed dtd_base_urls implementation
- factorized a lot of code in document patching

- better pretty printing on /update
- added stdout logger

added string_of_html_tag (plain text pretty printer for tags)

added support for multiple dtd_base_urls

updating all sections

patched

Bug fixed: the following happened.
Auto generated two goals.
Closing the first goal instantiated also the second goal.
But we were still iterating over the original list of goals ==> BOOM!

added exists_meta

patched

updating the introduction

ported to latest polymorphic variant types

Added flag test_equality_only to are_convertible to better implement
the <=_{\beta\delta\iota\zeta} relation.

Added flag test_equality_only to are_convertible (to better implement
the <=_{\beta\delta\iota\zeta} relation).

added a missing <br> tag

implemented save_to

- uncommented save_to function (now implemented)
- added (tiny) description of the 'variable interpolation' feature

added Unix dependency (needed in order to run xmllint)

eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing.

The parser accepts terms with metavariables as statements of theorems ==>
metavariable instantiation must be propagated also on the theorem statement.

- added test file

- added via_http parameter so that when the getter is used locally (i.e.
  as a library), http specific messages aren't generated
- use polymorphic variants for some configuration parameters
- better logging on /update (<br> tags are now generated)

- use polymorphic variants for some configuration parameters

bugfix: local context and canonical context previously don't have the
same length

bugfix: the function that abstract constant occurrences by putting metavariables
in place of identity explicit substitutions (local contexts) is generalized to
put ?1 : ?2 : Type in place of a ?1 : Type to take care of <Type in contravariant
position. Note: this is still partially bugged (see previous commit on the same
topic).

reorganized functions order

http_getter.conf.xml ==> /projects/helm/etc/http_getter.conf.xml

added html_of_html_tag

URL patching in ENTITY declarations extended to cover also absolute URLs.

XHTML character entities (used in the internal subset of .theory.xml files).

Added a new function in_cache to cicEnvironemt. It takes an uri
and returns true or false according to the fact that uri is or
is not in the cache

ht:DEFINITION/Definition differentiated into
 ht:DEFINITION/Definition and
 ht:DEFINITION/InteractiveDefinition

because of an explicit request of Iris Loeb.

s/per_user_settings/user_settings/ for consistency with gTopLevel
configuration file

- logging of long-running actions (like update) is now sent to the
  client incrementally
- moved some frontend related functions (like return_html*) from
  Http_getter_common to the frontend (main.ml)

removed no longer needed password from connection string

- added "Host:" line to http requests so that virtual hosting hosts are
  supported (and ancient HTTP are no longer supported)

- removed http_get/http_get_iter implementations, use the analogous
  functions from ocaml-http

<VARIABLE as="LocalFact"/> added

removed an out of date comment

added hyperlinks to help message

removed out of date configuration file

tacticChaser modified to avoid double "apply" and to avoid to apply uris ".var" in tactic "auto".

Meta files are in METAS subdir
source of meta files are called meta., not META.

Install to findlib-defined dest dir, not to stdlib dir

- provastruct.theory.xml removed (what was that exactly?)
- @name of SECTION renamed to @uri

updating and structuring

Algebra => CoRN

tex notation enabled

* the .o files to be used in the dll are now taken from the .libs subdirectoy
  (which presumably contains the PIC code)

CSC: hack to make applications of constants that have a Type sort which
occurs in contravariant position work. The idea is to generate in place
of a metavariable of type Type (that should be of type <Type) a
metavariable of type "a metavariable of type Type". The problem is that
in this way the metavariable can also be instantiated that is not a
sort.

* added embedding test (HTML)
* new things to do

* added TODO file

* added test with MathML really embedded within HTML
* set plugin border to 0 (? black line still visible)
* is set SHADOW_NONE the plugin window gets dirty!!! :-(

* implemented click so that the browser is notified with the new URL
  and loads it

cosmetic alignment change

- implemented real thread killing (in place of the previous fake implementation)

load_document(_,NULL) => unload

- power notation
- mult for BinInt

*** DANGEROUS ***
- multiple NUM instances now are different instances

...

introduction updated

The operational semantics of the core language is ready

Bug fixed for theorems whose statement are like

((A -> B) -> C) -> D

Sorts are no longer all convertible. To be completed once that universes are
implemented.

Sorts are no longer all convertible. To be completed once that universes
are implemented.

This fails.

added final version of the paper (for the records)