Commits · 73d08bfc98773f06356c44c6484614873f40b848 · Iris / Diaframe · GitLab

Snippets Groups Projects

Feb 18, 2022
- 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
- Made heap_lang 'simpl never', preventing cbn from unfolding it. · af6d9686
  Ike Mulder authored 3 years ago
  
  af6d9686
- Remove possibly costly call to auto in From/IntoTExist. · e35486ca
  Ike Mulder authored 3 years ago
  
  e35486ca
- Changed AsSolveGoal to hopefully reduce TC backtracking and speed up iStepDebug. · fe9eed71
  Ike Mulder authored 3 years ago
  
  fe9eed71
Feb 11, 2022
- Fixed forgotten instances of AsSolveGoal. · 82a79a00
  Ike Mulder authored 3 years ago
  
  82a79a00
- Removed pure argument to AsSolveGoal, abd_from_biabd priority is important! · b5fcc9df
  Ike Mulder authored 3 years ago
  
  b5fcc9df
- Removed duplication of environments in introducehyp lemmas. · db612532
  Ike Mulder authored 3 years ago
  
  db612532
- Replaced 'try cont' with 'cont', should avoid TC search on sideconditions when hints are not found. · 09611c06
  Ike Mulder authored 3 years ago
  
  09611c06
- Fixed definition of abd_step_hyp_mod. · f5794211
  Ike Mulder authored 3 years ago
  
  f5794211
Feb 10, 2022
- Fixed costly general recursive rhs modality instance, partially fixed running... · 85f32359
  Ike Mulder authored 3 years ago
  
  Fixed costly general recursive rhs modality instance, partially fixed running TC search too often for recursive hint search.
  85f32359
- Added timing tests for failing verifications, fixed mcs lock. · 4226453d
  Ike Mulder authored 3 years ago
  
  4226453d
- Added functionality to somewhat easily count distinct number of used hints. · 8a6a58c1
  Ike Mulder authored 3 years ago
  
  8a6a58c1
- Made bag stack faster by using more annotations.. but the proof is prettier. · ab76d526
  Ike Mulder authored 3 years ago
  
  ab76d526
- Fix reloc examples shortened by support for □. · 91224064
  Ike Mulder authored 3 years ago
  
  91224064