Commits · 45c1c97686314dc92c0374124fdb79cd1b36a3f7 · Iris / Diaframe · GitLab

Snippets Groups Projects

Mar 04, 2022
- Add LICENSE · 45c1c976
  Ike Mulder authored 3 years ago
  
  45c1c976
- Update README.md · 17d4fa49
  Ike Mulder authored 3 years ago
  
  17d4fa49
Mar 02, 2022
- Made warnings disappear about possibly missing external folder when building. · 5ce9973f
  Ike Mulder authored 3 years ago
  
  5ce9973f
Mar 01, 2022
- Added short comments at the top of most files. · ad3dc2b6
  Ike Mulder authored 3 years ago
  
  ad3dc2b6
- Updated _CoqProject_noext to new namespace. · 6f80af92
  Ike Mulder authored 3 years ago
  
  6f80af92
- Changed namespace to diaframe, improved local_post tactic. · ae690789
  Ike Mulder authored 3 years ago
  
  ae690789
Feb 22, 2022
- Updated irisexamples and lambda-rust. · 736b5567
  Ike Mulder authored 3 years ago
  
  736b5567
Feb 21, 2022
- Fix for no longer compiling with 8.13 and 8.14. · 57417937
  Ike Mulder authored 3 years ago
  
  57417937
- Update iris version dependency in opam file. · aa3c42cf
  Ike Mulder authored 3 years ago
  
  aa3c42cf
- Updating diaframe to recent iris version. · c1ef67d6
  Ike Mulder authored 3 years ago
  
  c1ef67d6
- Improved CLH lock proof. · 9070ba72
  Ike Mulder authored 3 years ago
  
  9070ba72
- Moved decompose_seps to legacy files. · b3c00995
  Ike Mulder authored 3 years ago
  
  b3c00995
Feb 18, 2022
- Ensured external examples still work, replaced rewrite /term with unfold for SolveSepSidecondition. · 86ff3e80
  Ike Mulder authored 3 years ago
  
  86ff3e80
- Added a template for goal transformer of pure execution, added a modality there for reloc. · 73d08bfc
  Ike Mulder authored 3 years ago
  
  73d08bfc
- Renamed biabd folder to hint_search. · ac878b7c
  Ike Mulder authored 3 years ago
  
  ac878b7c
- Better division of hints into library and real base hints. · da68cb13
  Ike Mulder authored 3 years ago
  
  da68cb13
- Fixed bad dependency on old compiled files. · 600ff005
  Ike Mulder authored 3 years ago
  
  600ff005
- Moved biabd_local_updates to library folder. · 27b6ea4e
  Ike Mulder authored 3 years ago
  
  27b6ea4e
Feb 17, 2022
- Changed MergablePersist to use <pers> instead of □, added support for introducing <pers> modality. · 370bad71
  Ike Mulder authored 3 years ago
  
  370bad71
- Test CI with proposed MR. · e5c61f7d
  Ike Mulder authored 3 years ago
  
  e5c61f7d
Feb 16, 2022
- Changed docker image to a new bullseye based fork. · 899d812c
  Ike Mulder authored 3 years ago
  
  899d812c
- Make 8.14 build with timing tag. · daf051de
  Ike Mulder authored 3 years ago
  
  daf051de
- Change CI branch. · 54d28922
  Ike Mulder authored 3 years ago
  
  54d28922
- Lowered max num of cores, see if this influences concurrent performance. · 808aa032
  Ike Mulder authored 3 years ago
  
  808aa032
Feb 15, 2022
- Fixed slower examples. · f6a33278
  Ike Mulder authored 3 years ago
  
  f6a33278
- Some thoughts on improving speed of log.atom verifications. · 4fb1664c
  Ike Mulder authored 3 years ago
  
  4fb1664c
- Fixed broken proofs caused by needing less iStepsS. · 4cd7e0d5
  Ike Mulder authored 3 years ago
  
  4cd7e0d5
- Fixed improved pure execution instance being passed over. · 47fc6fee
  Ike Mulder authored 3 years ago
  
  47fc6fee
- Got rid of FromTSep, replaced by using TC∀. · 6841d0e1
  Ike Mulder authored 3 years ago
  
  6841d0e1
- Using matches to hopefully speed up introduceHyp. · d345122b
  Ike Mulder authored 3 years ago
  
  d345122b
- Added shortcircuiting on premise shape for abduct hint search. · 507b8706
  Ike Mulder authored 3 years ago
  
  507b8706
- Apparently 'rewrite /term' is way slower than 'unfold term'. · 5e3705ea
  Ike Mulder authored 3 years ago
  
  5e3705ea
- Fixed putting TC∀ in too many places. · 07415805
  Ike Mulder authored 3 years ago
  
  07415805
- Introduced specialized typeclass for ∀.. search. · 8bb2b148
  Ike Mulder authored 3 years ago
  
  8bb2b148
- Testing out sealed off definitions of proof state. · acf488aa
  Ike Mulder authored 3 years ago
  
  acf488aa
- Defining MergablePersist with <pers> seems to suit non-affine logics better. · 21cf6b4e
  Ike Mulder authored 3 years ago
  
  21cf6b4e
Feb 14, 2022
- Testing out possibly improved PureExec reductionstep. · ce65e4f6
  Ike Mulder authored 3 years ago
  
  ce65e4f6
- Made previous change more surgical. · 4572479c
  Ike Mulder authored 3 years ago
  
  4572479c
- Slight change to hint search, to fix support for separating Laterable things. · e3fd032f
  Ike Mulder authored 3 years ago
  
  e3fd032f
- Removed calling iDecomposeSeps every iStep call, unused and somewhat costly. · f8073c5c
  Ike Mulder authored 3 years ago
  
  f8073c5c