made executable again

Merge branch 'dune' of git+ssh://matita.cs.unibo.it/srv/git/helm into dune

Ctr-C/break button behaviour fixed

new executables (ported by Ferruccio Guidi)

mod change (-x)

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

Ctr-C/break button behaviour fixed

new executables (ported by Ferruccio Guidi)

mod change (-x)

wip ....

+ a situation in which matita falls asleep was detected

update from master branch

update in delayed_updating

+ new operator on update functions

update in ground

+ some additions
+ some renaming

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

+ 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