]>
matita.cs.unibo.it Git - helm.git/log
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)
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:36:37 +0000 (00:36 +0100)]
Remove dandling symbolic links from the repository
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:32:27 +0000 (00:32 +0100)]
Use source and licence accepted by opam
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:20:01 +0000 (00:20 +0100)]
Install what is needed by Matita (but not used yet!)
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:19:15 +0000 (00:19 +0100)]
make_table is now private (= not installed)
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 23:19:01 +0000 (00:19 +0100)]
I forgot Luca among the authors!
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
Claudio Sacerdoti Coen [Mon, 2 Jan 2023 20:46:29 +0000 (21:46 +0100)]
Generated files (for dune) added to .gitignore
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.
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)
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)
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.
Claudio Sacerdoti Coen [Fri, 30 Dec 2022 21:23:44 +0000 (22:23 +0100)]
Ctr-C now is equivalent to pressing the Break button
Claudio Sacerdoti Coen [Fri, 30 Dec 2022 20:31:23 +0000 (21:31 +0100)]
Avoid race conditions (deadlocks)
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
Ferruccio Guidi [Wed, 18 Jan 2023 20:47:29 +0000 (21:47 +0100)]
update in delayed_updating
+ new operator on update functions
Ferruccio Guidi [Wed, 18 Jan 2023 19:56:10 +0000 (20:56 +0100)]
update in ground
+ some additions
+ some renaming
Ferruccio Guidi [Wed, 28 Dec 2022 16:47:38 +0000 (17:47 +0100)]
update in delayed_updating
+ some renaming
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
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
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
Ferruccio Guidi [Mon, 19 Dec 2022 22:16:18 +0000 (23:16 +0100)]
update in ground
+ some renaming
Ferruccio Guidi [Wed, 14 Dec 2022 21:15:07 +0000 (22:15 +0100)]
update in delayed_updating
+ guard condition removed from reduction
Ferruccio Guidi [Wed, 14 Dec 2022 18:37:46 +0000 (19:37 +0100)]
update in ground
+ minor addition to relocation
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
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
Ferruccio Guidi [Wed, 23 Nov 2022 08:33:26 +0000 (09:33 +0100)]
wip in delayed_updating
guard condition
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
Ferruccio Guidi [Mon, 14 Nov 2022 22:13:29 +0000 (23:13 +0100)]
update in delayed_updating
+ example of unprotected balanced reduction continued
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
Ferruccio Guidi [Sat, 12 Nov 2022 22:21:34 +0000 (23:21 +0100)]
update in ground
+ positive integer two
Ferruccio Guidi [Sun, 6 Nov 2022 18:24:03 +0000 (19:24 +0100)]
update in ground
+ additions to subset extensionality
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
Ferruccio Guidi [Wed, 2 Nov 2022 17:30:43 +0000 (18:30 +0100)]
update in delayed_updating
commutations of balanced reduction completed
Ferruccio Guidi [Wed, 26 Oct 2022 21:43:23 +0000 (23:43 +0200)]
update in predefined_virtuals
+ two arrows added
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
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
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
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
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
Ferruccio Guidi [Sun, 4 Sep 2022 19:30:07 +0000 (21:30 +0200)]
update in delayd_updating
+ introduction of path_closed complete
Ferruccio Guidi [Sun, 4 Sep 2022 19:25:25 +0000 (21:25 +0200)]
update in ground
+ some renaming and some refactoring
Ferruccio Guidi [Tue, 23 Aug 2022 16:18:57 +0000 (18:18 +0200)]
update in static_2
+ notation update from ground
Ferruccio Guidi [Tue, 23 Aug 2022 16:17:59 +0000 (18:17 +0200)]
update in ground
+ notation update and renaming
Ferruccio Guidi [Sun, 21 Aug 2022 22:44:42 +0000 (00:44 +0200)]
addition to predefined virtuals
+ one character added
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
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
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
Ferruccio Guidi [Tue, 9 Aug 2022 21:02:25 +0000 (23:02 +0200)]
commit in delayed_updating
+ reversing paths completed updating component "reduction"
Ferruccio Guidi [Sun, 7 Aug 2022 17:37:11 +0000 (19:37 +0200)]
update in ground
+ additions to nap and xap
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
Ferruccio Guidi [Sat, 6 Aug 2022 22:20:11 +0000 (00:20 +0200)]
partial commit in delayed_updating
+ reversing paths in component "unwind"
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
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
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
Ferruccio Guidi [Wed, 6 Jul 2022 12:21:03 +0000 (14:21 +0200)]
update in ground
+ one more lemma with list_append
Ferruccio Guidi [Wed, 6 Jul 2022 12:18:48 +0000 (14:18 +0200)]
partial commit in delayed_updating
+ parchin reverse operator for paths
Ferruccio Guidi [Wed, 29 Jun 2022 22:53:46 +0000 (00:53 +0200)]
update in delayed_updating
+ bind condition simplified for ifr and dfr
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
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
Ferruccio Guidi [Sat, 25 Jun 2022 21:01:12 +0000 (23:01 +0200)]
update in delayed_updating
+ some additions
+ minor improvements
Ferruccio Guidi [Fri, 24 Jun 2022 21:48:36 +0000 (23:48 +0200)]
update in delayed_updating
+ ifr_lift proved
+ ifr corrected
+ minor corrections
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
Ferruccio Guidi [Wed, 22 Jun 2022 11:38:45 +0000 (13:38 +0200)]
update in ground
+ minor corrections
Ferruccio Guidi [Wed, 22 Jun 2022 11:38:11 +0000 (13:38 +0200)]
update in delayed updating
+ dfr_lift_bi proved
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
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
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
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
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
Ferruccio Guidi [Wed, 8 Jun 2022 18:27:49 +0000 (20:27 +0200)]
update in ground
* subset overlap
Ferruccio Guidi [Wed, 8 Jun 2022 17:49:26 +0000 (19:49 +0200)]
update in lib
+ notation for overlap decentralized
Ferruccio Guidi [Wed, 8 Jun 2022 17:14:49 +0000 (19:14 +0200)]
update in delayed_updating
+ some files parked
Ferruccio Guidi [Mon, 30 May 2022 21:50:58 +0000 (23:50 +0200)]
update in delayed_updating
+ lift: additions and refactoring
+ reduction: WIP
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
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
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
Ferruccio Guidi [Fri, 20 May 2022 20:43:51 +0000 (22:43 +0200)]
update in ground
+ additions to lifts
Ferruccio Guidi [Thu, 19 May 2022 10:11:11 +0000 (12:11 +0200)]
update in ground
+ new notation for application of a relocation
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
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
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
Ferruccio Guidi [Thu, 5 May 2022 12:15:52 +0000 (14:15 +0200)]
update in delayed_updating
+ notation for reversed path
Ferruccio Guidi [Tue, 3 May 2022 20:45:16 +0000 (22:45 +0200)]
update in delayed_updating
+ conflicts solved
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
Ferruccio Guidi [Tue, 3 May 2022 17:46:49 +0000 (19:46 +0200)]
update in delayed_updating
+ some notation updated
+ some unused files removed
Ferruccio Guidi [Thu, 28 Apr 2022 15:34:11 +0000 (17:34 +0200)]
update in delayed_updating
+ alternative definition of unwind based on lift
Ferruccio Guidi [Thu, 28 Apr 2022 12:29:08 +0000 (14:29 +0200)]
update in delayed updating
updated notation
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
Ferruccio Guidi [Wed, 27 Apr 2022 17:34:39 +0000 (19:34 +0200)]
update in ground
+ some addittions and corrections
Ferruccio Guidi [Wed, 27 Apr 2022 17:24:30 +0000 (19:24 +0200)]
update un delayed updating
+ some parked files
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
Ferruccio Guidi [Sat, 26 Mar 2022 20:12:19 +0000 (21:12 +0100)]
update in delayed updating
+ additions to lift
Ferruccio Guidi [Sat, 26 Mar 2022 16:56:36 +0000 (17:56 +0100)]
update in ground
+ some additions and corrections
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
Ferruccio Guidi [Wed, 16 Mar 2022 21:41:40 +0000 (22:41 +0100)]
update in delayed_updating
+ some additions and corrections
Ferruccio Guidi [Wed, 16 Mar 2022 21:32:37 +0000 (22:32 +0100)]
update in ground
+ some additions
Ferruccio Guidi [Tue, 1 Mar 2022 00:14:15 +0000 (01:14 +0100)]
partial update in delayed_updating
+ WIP
Ferruccio Guidi [Tue, 1 Mar 2022 00:12:44 +0000 (01:12 +0100)]
update in ground
+ minor corrections and additions
Ferruccio Guidi [Wed, 16 Feb 2022 22:45:20 +0000 (23:45 +0100)]
update in delayed_updating
+ important additionsand corrections