wip ....

+ a situation in which matita falls asleep was detected

unused componentsConf module removed

auxiliary executables (xoa, matitadep, probe, matex) ported to dune

revert from camlp5o to standard syntax

Dependency on ocaml_http replaced by ocaml_http_stubs stubs

- the stubs always fail with an assert false
- the code is still live in Matita, but currently unused in practice
- ocaml_http depends on ocamlnet, that is way too hard to port completely
  to ocaml 5.0.0. A better path to restore the lost functionalities is
  to reimplement ocaml_http_stubs on modern libraries (e.g. lwt-cohttp)

camlp5.gramlib does not pull in camlp-streams by default

registry already did not depend on ocamlnet any more

allow ocaml >= 4.14.1

All previously auto-generated files from *.in committed

- the values are surely wrong, even if they should be mostly unused
  or set by hand at each release

Once I will figure out what to do correctly, I will remove the .in files
too.

METAS removed + matita.conf.xml committed

Bad spelling for camlzip

Added dependency on caml-zip

Added dependency on ocaml-http

In last commit I forgot to regenerate matita.opam :-(

Added pcre + depenencies relaxed using >=

Drop zip dependency (no longer used)

Remove all traces of autoconf/automake/makefile

- also fixes installation of help/C files to include only .xml files
  and figures

comment removed

Install into doc the PDF and HTML manuals

Ignore *-stamp in matita/help/C

Manual(s) fixed and committed to avoid rebuilding them in dune

- fixed a bug in the XSLT that used wrong linkends
- the HTML and PDF files are now committed to the repository

Note: there is a now old (4 years!) but in yelp with links to other
pages in XMLDOCs. Not my fault, but most hyperlinks are broken.

Makefiles removed in favour of dune-only solution

- some Makefiles are still to be removed
- some Makefiles in legacy dirs that are no longer compiled will
  be kept
- the Makefile in help is still useful!

added comment about version number to be manually changed

Dune sites used to locate the standard library

- it works both before and after installation
- it definitely breaks the Makefiles

Use dune-build-info to put the version in buildTimeConf

componentsConf is unused (and automatically generated)

Do not compile it (to get rid of Makefile)

Remove dandling symbolic links from the repository

Use source and licence accepted by opam

Install what is needed by Matita (but not used yet!)

make_table is now private (= not installed)

I forgot Luca among the authors!

Enable "dune build -p matita" + version bumped to 0.99.5

Generated files (for dune) added to .gitignore

Fix "dune build" for syntax_extensions

- pa_unicode_macro.cma no longer "includes" helm_syntax_extensions.cma

The only reason for this change, that makes camlp5o harder to call, is
that dune enforces modules to belong to one library only.

Preliminary support for dune

- dune build matita/matita{,c,clean}.exe works
- dune build fails on components/syntax_extensions where we need
  to add modules to two different libraries. I have found a
  workaround (dune does not allow it!) that works when building
  matita*.exe, but not when doing "dune build"
- the dune files and the Makefiles are not 100% equivalent
  (e.g. some modules not dropped during compilation, the user
  interface not generated by glade yet)

Use of standard OCaml syntax

- do not rely on camlp5o for many files
- comply with the most recent OCaml warnings
- gtkMisc splitted into gtkMisc and gtkMiscCli, the latter
  does not depend on Gtk
- matitaclean is no longer a symbolic link to matita
  (required to switch to dune)

Worker thread killing fixed

In old Ocaml it used to work catching a Unix signal that was raised at the
end of each timeslice. It works no more in Ocaml5.

- we now use a fixed timer (every 1s) to trigger the Unix signal
- the signal is usually caught by the non-worker thread and for some reason
  blocking the signal interferes with Gtk
- solution: if the signal is caught by the non-worker thread, the thread
  goes to sleep for 3s to let the worker thread catch the signal

Most of the time the trick works, even if some delay is introdued.

Ctr-C now is equivalent to pressing the Break button

Avoid race conditions (deadlocks)

Porting to ocaml 5

- old hashing dropped from ocaml code => hash.c is not part of ng_paramodulation
- as a consequence, bytecode is now compile in -custom mode
- requires patched versions of ocaml-expant, ocamlnet and ulex-camlp5
  (all currently not accepted upstream yet)
- plenty of new warnings either turned off or applied to code
- ported to most recent version of camlp5

update in delayed_updating

+ new operator on update functions

update in ground

+ some additions
+ some renaming

update in delayed_updating

+ some renaming

update in delayed_updating

+ more complex example in which discarding num labels in b solves unwind

update in delayed_updating

+ couterexample to dbfr_ibfr when inner labels in b are not bound in b

update in delayed_updating

+ excess added to closure condition for path
+ height for path restored

update in ground

+ some renaming

update in delayed_updating

+ guard condition removed from reduction

update in ground

+ minor addition to relocation

update in delayed_updating

+ bug fixed in the "crux of the proof" allows to certify more reductions
+ restricted form of closed path not used anymore

update in ground

+ head-tail decomposition of a relocation map
+ injectivity of pnpred

wip in delayed_updating

guard condition

update in delayed_updating

+ example of unprotected balanced reduction continued and simplified

update in delayed_updating

+ example of unprotected balanced reduction continued

update in delayed_updating

+ example of unprotected balanced β-reduction started
+ some corrections and additions

update in ground

+ positive integer two

update in ground

+ additions to subset extensionality

update in delayed_updating

+ core reduction parked
+ paths of one repeated label resumed

update in delayed_updating

commutations of balanced reduction completed

update in predefined_virtuals

+ two arrows added

update in delayed_updating

+ balanced reduction with main theorem proved
+ notation change for lift

update in delayed_updating and ground

+ single specification for protected and unprotected closed path
+ some parked files removed

update in delayed_updating

+ reference by depth with offset parked for now

partial update in delayed_updating

+ we add reference by depth with offset
+ component "syntax" updated
+ some improvements
+ height parked for now

update in ground and delayed_updating

+ example of unprotected balanced segment
+ balanced reduction parked for now
+ additions and renaming

update in delayd_updating

+ introduction of path_closed complete

update in ground

+ some renaming and some refactoring

update in static_2

+ notation update from ground

update in ground

+ notation update and renaming

addition to predefined virtuals

+ one character added

partial update in delayed_updating

+ syntax and substitution components updated
+ path_head parked and replaced by path_closed
+ balanced reductions introduced and main theorem proved
+ minor corrections to notation

update in delayed_updating

+ focused reduction takes just one focus
+ changed minor premise of ifr_unwind_bi
+ some renaming

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

commit in delayed_updating

+ reversing paths completed updating component "reduction"

update in ground

+ additions to nap and xap

update in delayed_updating

+ three old lemmas restored
+ some parked lemmas removed
+ minor renaming

partial commit in delayed_updating

+ reversing paths in component "unwind"

partial commit in delayed_updating

+ reversing paths in component "substitution"
+ lift reformulated in terms of simpler functions

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

partial commit in delayed_updating

+ reversing paths in component "syntax"
+ some renaming

update in ground

+ one more lemma with list_append

partial commit in delayed_updating

+ parchin reverse operator for paths

update in delayed_updating

+ bind condition simplified for ifr and dfr

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

update in delayed updating

+ two lemmas on path_head
+ invocation added to first file

update in delayed_updating

+ some additions
+ minor improvements

update in delayed_updating

+ ifr_lift proved
+ ifr corrected
+ minor corrections

update in delayed_updating

+ unwind2_path_after_lift
+ prelift
+ refactoring for lift

update in ground

+ minor corrections

update in delayed updating

+ dfr_lift_bi proved

update in delayed_updating

+ WIP on lift
+ notation changed for delayed updating (term constructor)
+ minor corrections

update in delayed_updating

+ additions for lift
+ advances in dfr_lift_bi
+ some corrections
+ some parked files removed

update in delayed_updating

+ final definition of lift
+ WIP on dfr_lift_bi
+ updates and corrections
+ old definition of lift parked

update in delayed_updating

+ bug fixed in ifr allows to prove ifr_unwind_bi

update in delayed_updating

+ lift changed to lift after unwind in ifr
+ notion of lift swapped again
+ some additions to prove a side condition of ifr_unwind_bi

update in ground

* subset overlap

update  in lib

+ notation for overlap decentralized

update in delayed_updating

+ some files parked

update in delayed_updating

+ lift: additions and refactoring
+ reduction: WIP

update in ground and delayed_updating

+ main theorem about dfr proved!
+ ground: duplicated lemma removed
+ some refactoring