]> matita.cs.unibo.it Git - helm.git/log
helm.git
20 months agocomponentsConf is unused (and automatically generated)
Claudio Sacerdoti Coen [Tue, 3 Jan 2023 00:56:28 +0000 (01:56 +0100)]
componentsConf is unused (and automatically generated)

Do not compile it (to get rid of Makefile)

20 months agoRemove dandling symbolic links from the repository
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:36:37 +0000 (00:36 +0100)]
Remove dandling symbolic links from the repository

20 months agoUse source and licence accepted by opam
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:32:27 +0000 (00:32 +0100)]
Use source and licence accepted by opam

20 months agoInstall what is needed by Matita (but not used yet!)
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:20:01 +0000 (00:20 +0100)]
Install what is needed by Matita (but not used yet!)

20 months agomake_table is now private (= not installed)
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:19:15 +0000 (00:19 +0100)]
make_table is now private (= not installed)

20 months agoI forgot Luca among the authors!
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:19:01 +0000 (00:19 +0100)]
I forgot Luca among the authors!

20 months agoEnable "dune build -p matita" + version bumped to 0.99.5
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 21:29:33 +0000 (22:29 +0100)]
Enable "dune build -p matita" + version bumped to 0.99.5

20 months agoGenerated files (for dune) added to .gitignore
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 20:46:29 +0000 (21:46 +0100)]
Generated files (for dune) added to .gitignore

20 months agoFix "dune build" for syntax_extensions
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 19:56:40 +0000 (20:56 +0100)]
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.

20 months agoPreliminary support for dune
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 19:42:56 +0000 (20:42 +0100)]
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)

20 months agoUse of standard OCaml syntax
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 19:39:10 +0000 (20:39 +0100)]
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)

20 months agoWorker thread killing fixed
Claudio Sacerdoti Coen [Fri, 30 Dec 2022 21:27:33 +0000 (22:27 +0100)]
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.

20 months agoCtr-C now is equivalent to pressing the Break button
Claudio Sacerdoti Coen [Fri, 30 Dec 2022 21:23:44 +0000 (22:23 +0100)]
Ctr-C now is equivalent to pressing the Break button

20 months agoAvoid race conditions (deadlocks)
Claudio Sacerdoti Coen [Fri, 30 Dec 2022 20:31:23 +0000 (21:31 +0100)]
Avoid race conditions (deadlocks)

20 months agoPorting to ocaml 5
Claudio Sacerdoti Coen [Fri, 30 Dec 2022 01:19:16 +0000 (02:19 +0100)]
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

21 months agoupdate in delayed_updating
Ferruccio Guidi [Wed, 18 Jan 2023 20:47:29 +0000 (21:47 +0100)]
update in delayed_updating

+ new operator on update functions

21 months agoupdate in ground
Ferruccio Guidi [Wed, 18 Jan 2023 19:56:10 +0000 (20:56 +0100)]
update in ground

+ some additions
+ some renaming

22 months agoupdate in delayed_updating
Ferruccio Guidi [Wed, 28 Dec 2022 16:47:38 +0000 (17:47 +0100)]
update in delayed_updating

+ some renaming

22 months agoupdate in delayed_updating
Ferruccio Guidi [Tue, 27 Dec 2022 16:08:00 +0000 (17:08 +0100)]
update in delayed_updating

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

22 months agoupdate in delayed_updating
Ferruccio Guidi [Wed, 21 Dec 2022 15:33:06 +0000 (16:33 +0100)]
update in delayed_updating

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

22 months agoupdate in delayed_updating
Ferruccio Guidi [Tue, 20 Dec 2022 00:10:07 +0000 (01:10 +0100)]
update in delayed_updating

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

22 months agoupdate in ground
Ferruccio Guidi [Mon, 19 Dec 2022 22:16:18 +0000 (23:16 +0100)]
update in ground

+ some renaming

22 months agoupdate in delayed_updating
Ferruccio Guidi [Wed, 14 Dec 2022 21:15:07 +0000 (22:15 +0100)]
update in delayed_updating

+ guard condition removed from reduction

22 months agoupdate in ground
Ferruccio Guidi [Wed, 14 Dec 2022 18:37:46 +0000 (19:37 +0100)]
update in ground

+ minor addition to relocation

22 months agoupdate in delayed_updating
Ferruccio Guidi [Sun, 11 Dec 2022 18:29:08 +0000 (19:29 +0100)]
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

22 months agoupdate in ground
Ferruccio Guidi [Wed, 7 Dec 2022 16:46:39 +0000 (17:46 +0100)]
update in ground

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

23 months agowip in delayed_updating
Ferruccio Guidi [Wed, 23 Nov 2022 08:33:26 +0000 (09:33 +0100)]
wip in delayed_updating

guard condition

23 months agoupdate in delayed_updating
Ferruccio Guidi [Thu, 17 Nov 2022 22:08:19 +0000 (23:08 +0100)]
update in delayed_updating

+ example of unprotected balanced reduction continued and simplified

23 months agoupdate in delayed_updating
Ferruccio Guidi [Mon, 14 Nov 2022 22:13:29 +0000 (23:13 +0100)]
update in delayed_updating

+ example of unprotected balanced reduction continued

23 months agoupdate in delayed_updating
Ferruccio Guidi [Sun, 13 Nov 2022 22:34:18 +0000 (23:34 +0100)]
update in delayed_updating

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

23 months agoupdate in ground
Ferruccio Guidi [Sat, 12 Nov 2022 22:21:34 +0000 (23:21 +0100)]
update in ground

+ positive integer two

23 months agoupdate in ground
Ferruccio Guidi [Sun, 6 Nov 2022 18:24:03 +0000 (19:24 +0100)]
update in ground

+ additions to subset extensionality

23 months agoupdate in delayed_updating
Ferruccio Guidi [Sun, 6 Nov 2022 18:21:23 +0000 (19:21 +0100)]
update in delayed_updating

+ core reduction parked
+ paths of one repeated label resumed

23 months agoupdate in delayed_updating
Ferruccio Guidi [Wed, 2 Nov 2022 17:30:43 +0000 (18:30 +0100)]
update in delayed_updating

commutations of balanced reduction completed

2 years agoupdate in predefined_virtuals
Ferruccio Guidi [Wed, 26 Oct 2022 21:43:23 +0000 (23:43 +0200)]
update in predefined_virtuals

+ two arrows added

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 26 Oct 2022 21:42:31 +0000 (23:42 +0200)]
update in delayed_updating

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

2 years agoupdate in delayed_updating and ground
Ferruccio Guidi [Tue, 25 Oct 2022 22:02:00 +0000 (00:02 +0200)]
update in delayed_updating and ground

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

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sun, 11 Sep 2022 21:13:53 +0000 (23:13 +0200)]
update in delayed_updating

+ reference by depth with offset parked for now

2 years agopartial update in delayed_updating
Ferruccio Guidi [Thu, 8 Sep 2022 11:02:59 +0000 (13:02 +0200)]
partial update in delayed_updating

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

2 years agoupdate in ground and delayed_updating
Ferruccio Guidi [Wed, 7 Sep 2022 22:13:21 +0000 (00:13 +0200)]
update in ground and delayed_updating

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

2 years agoupdate in delayd_updating
Ferruccio Guidi [Sun, 4 Sep 2022 19:30:07 +0000 (21:30 +0200)]
update in delayd_updating

+ introduction of path_closed complete

2 years agoupdate in ground
Ferruccio Guidi [Sun, 4 Sep 2022 19:25:25 +0000 (21:25 +0200)]
update in ground

+ some renaming and some refactoring

2 years agoupdate in static_2
Ferruccio Guidi [Tue, 23 Aug 2022 16:18:57 +0000 (18:18 +0200)]
update in static_2

+ notation update from ground

2 years agoupdate in ground
Ferruccio Guidi [Tue, 23 Aug 2022 16:17:59 +0000 (18:17 +0200)]
update in ground

+ notation update and renaming

2 years agoaddition to predefined virtuals
Ferruccio Guidi [Sun, 21 Aug 2022 22:44:42 +0000 (00:44 +0200)]
addition to predefined virtuals

+ one character added

2 years agopartial update in delayed_updating
Ferruccio Guidi [Sun, 21 Aug 2022 22:43:28 +0000 (00:43 +0200)]
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

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sun, 14 Aug 2022 16:02:46 +0000 (18:02 +0200)]
update in delayed_updating

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

2 years agoMerge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm
Ferruccio Guidi [Tue, 9 Aug 2022 21:03:15 +0000 (23:03 +0200)]
Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

2 years agocommit in delayed_updating
Ferruccio Guidi [Tue, 9 Aug 2022 21:02:25 +0000 (23:02 +0200)]
commit in delayed_updating

+ reversing paths completed updating component "reduction"

2 years agoupdate in ground
Ferruccio Guidi [Sun, 7 Aug 2022 17:37:11 +0000 (19:37 +0200)]
update in ground

+ additions to nap and xap

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sun, 7 Aug 2022 17:36:15 +0000 (19:36 +0200)]
update in delayed_updating

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

2 years agopartial commit in delayed_updating
Ferruccio Guidi [Sat, 6 Aug 2022 22:20:11 +0000 (00:20 +0200)]
partial commit in delayed_updating

+ reversing paths in component "unwind"

2 years agopartial commit in delayed_updating
Ferruccio Guidi [Wed, 13 Jul 2022 18:19:56 +0000 (20:19 +0200)]
partial commit in delayed_updating

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

2 years agoMerge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm
Ferruccio Guidi [Wed, 6 Jul 2022 12:25:08 +0000 (14:25 +0200)]
Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

2 years agopartial commit in delayed_updating
Ferruccio Guidi [Wed, 6 Jul 2022 12:23:57 +0000 (14:23 +0200)]
partial commit in delayed_updating

+ reversing paths in component "syntax"
+ some renaming

2 years agoupdate in ground
Ferruccio Guidi [Wed, 6 Jul 2022 12:21:03 +0000 (14:21 +0200)]
update in ground

+ one more lemma with list_append

2 years agopartial commit in delayed_updating
Ferruccio Guidi [Wed, 6 Jul 2022 12:18:48 +0000 (14:18 +0200)]
partial commit in delayed_updating

+ parchin reverse operator for paths

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 29 Jun 2022 22:53:46 +0000 (00:53 +0200)]
update in delayed_updating

+ bind condition simplified for ifr and dfr

2 years agoMerge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm
Ferruccio Guidi [Wed, 29 Jun 2022 12:23:12 +0000 (14:23 +0200)]
Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

2 years agoupdate in delayed updating
Ferruccio Guidi [Wed, 29 Jun 2022 12:22:26 +0000 (14:22 +0200)]
update in delayed updating

+ two lemmas on path_head
+ invocation added to first file

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sat, 25 Jun 2022 21:01:12 +0000 (23:01 +0200)]
update in delayed_updating

+ some additions
+ minor improvements

2 years agoupdate in delayed_updating
Ferruccio Guidi [Fri, 24 Jun 2022 21:48:36 +0000 (23:48 +0200)]
update in delayed_updating

+ ifr_lift proved
+ ifr corrected
+ minor corrections

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 23 Jun 2022 10:54:36 +0000 (12:54 +0200)]
update in delayed_updating

+ unwind2_path_after_lift
+ prelift
+ refactoring for lift

2 years agoupdate in ground
Ferruccio Guidi [Wed, 22 Jun 2022 11:38:45 +0000 (13:38 +0200)]
update in ground

+ minor corrections

2 years agoupdate in delayed updating
Ferruccio Guidi [Wed, 22 Jun 2022 11:38:11 +0000 (13:38 +0200)]
update in delayed updating

+ dfr_lift_bi proved

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 20 Jun 2022 23:33:06 +0000 (01:33 +0200)]
update in delayed_updating

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

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 15 Jun 2022 22:47:11 +0000 (00:47 +0200)]
update in delayed_updating

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

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 13 Jun 2022 22:30:57 +0000 (00:30 +0200)]
update in delayed_updating

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

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 9 Jun 2022 13:39:52 +0000 (15:39 +0200)]
update in delayed_updating

+ bug fixed in ifr allows to prove ifr_unwind_bi

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 8 Jun 2022 22:43:41 +0000 (00:43 +0200)]
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

2 years agoupdate in ground
Ferruccio Guidi [Wed, 8 Jun 2022 18:27:49 +0000 (20:27 +0200)]
update in ground

* subset overlap

2 years agoupdate in lib
Ferruccio Guidi [Wed, 8 Jun 2022 17:49:26 +0000 (19:49 +0200)]
update  in lib

+ notation for overlap decentralized

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 8 Jun 2022 17:14:49 +0000 (19:14 +0200)]
update in delayed_updating

+ some files parked

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 30 May 2022 21:50:58 +0000 (23:50 +0200)]
update in delayed_updating

+ lift: additions and refactoring
+ reduction: WIP

2 years agoupdate in ground and delayed_updating
Ferruccio Guidi [Wed, 25 May 2022 18:38:32 +0000 (20:38 +0200)]
update in ground and delayed_updating

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

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 23 May 2022 22:39:34 +0000 (00:39 +0200)]
update in delayed_updating

+ crux of the main proof completed
+ notation for path_reverse fixed

2 years agoupdate in delayed_updating
Ferruccio Guidi [Sat, 21 May 2022 18:23:22 +0000 (20:23 +0200)]
update in delayed_updating

+ unwind completed with an important result on lift

2 years agoupdate in ground
Ferruccio Guidi [Fri, 20 May 2022 20:43:51 +0000 (22:43 +0200)]
update in ground

+ additions to lifts

2 years agoupdate in ground
Ferruccio Guidi [Thu, 19 May 2022 10:11:11 +0000 (12:11 +0200)]
update in ground

+ new notation for application of a relocation

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 17 May 2022 19:09:39 +0000 (21:09 +0200)]
update in delayed_updating

+ generic unwind meeds to be  even more generic

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 17 May 2022 15:51:39 +0000 (17:51 +0200)]
update in delayed_updating

+ generic unwind for path
+ some old files parked

2 years agoupdate in delayed_updating
Ferruccio Guidi [Mon, 9 May 2022 19:08:36 +0000 (21:08 +0200)]
update in delayed_updating

+ main function to locate the referred binder
+ update function for unfold

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 5 May 2022 12:15:52 +0000 (14:15 +0200)]
update in delayed_updating

+ notation for reversed path

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 3 May 2022 20:45:16 +0000 (22:45 +0200)]
update in delayed_updating

+ conflicts solved

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 3 May 2022 18:31:58 +0000 (20:31 +0200)]
update in delayed_updating

+ closed paths
+ updated notation for height
+ some parked files added

2 years agoupdate in delayed_updating
Ferruccio Guidi [Tue, 3 May 2022 17:46:49 +0000 (19:46 +0200)]
update in delayed_updating

+ some notation updated
+ some unused files removed

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 28 Apr 2022 15:34:11 +0000 (17:34 +0200)]
update in delayed_updating

+ alternative definition of unwind based on lift

2 years agoupdate in delayed updating
Ferruccio Guidi [Thu, 28 Apr 2022 12:29:08 +0000 (14:29 +0200)]
update in delayed updating

updated notation

2 years agoupdate in delayed updating
Ferruccio Guidi [Wed, 27 Apr 2022 17:41:11 +0000 (19:41 +0200)]
update in delayed updating

+ new version of lift
+ corrected and updated notation

2 years agoupdate in ground
Ferruccio Guidi [Wed, 27 Apr 2022 17:34:39 +0000 (19:34 +0200)]
update in ground

+ some addittions and corrections

2 years agoupdate un delayed updating
Ferruccio Guidi [Wed, 27 Apr 2022 17:24:30 +0000 (19:24 +0200)]
update un delayed updating

+ some parked files

2 years agoWIP in delayed_updating
Ferruccio Guidi [Mon, 28 Mar 2022 23:11:32 +0000 (01:11 +0200)]
WIP in delayed_updating

+ we re focusing on a special case of the main theorem

2 years agoupdate in delayed updating
Ferruccio Guidi [Sat, 26 Mar 2022 20:12:19 +0000 (21:12 +0100)]
update in delayed updating

+ additions to lift

2 years agoupdate in ground
Ferruccio Guidi [Sat, 26 Mar 2022 16:56:36 +0000 (17:56 +0100)]
update in ground

+ some additions and corrections

2 years agoupdate in delayed_updating
Ferruccio Guidi [Thu, 24 Mar 2022 20:08:45 +0000 (21:08 +0100)]
update in delayed_updating

+ lift
+ two versions of unwind
+ some renaming, additions and corrections

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 16 Mar 2022 21:41:40 +0000 (22:41 +0100)]
update in delayed_updating

+ some additions and corrections

2 years agoupdate in ground
Ferruccio Guidi [Wed, 16 Mar 2022 21:32:37 +0000 (22:32 +0100)]
update in ground

+ some additions

2 years agopartial update in delayed_updating
Ferruccio Guidi [Tue, 1 Mar 2022 00:14:15 +0000 (01:14 +0100)]
partial update in delayed_updating

+ WIP

2 years agoupdate in ground
Ferruccio Guidi [Tue, 1 Mar 2022 00:12:44 +0000 (01:12 +0100)]
update in ground

+ minor corrections and additions

2 years agoupdate in delayed_updating
Ferruccio Guidi [Wed, 16 Feb 2022 22:45:20 +0000 (23:45 +0100)]
update in delayed_updating

+ important additionsand corrections