Diaframe issueshttps://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues2022-03-29T11:23:53Zhttps://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues/12Consistent variable and hypothesis naming2022-03-29T11:23:53ZIke MulderConsistent variable and hypothesis namingChanges in the implementation and in the available hints can cause changes in variable names, which is unwanted.
Different versions of Iris have also sometimes caused different hypotheses names, also unwanted.
Idea to get consistent hyp...Changes in the implementation and in the available hints can cause changes in variable names, which is unwanted.
Different versions of Iris have also sometimes caused different hypotheses names, also unwanted.
Idea to get consistent hypotheses names: don't use the IPM environment, instead use a custom list environment, and change back to the IPM env after a tactic finishes.
Idea to get consistent variable names: look at how IPM does it for foralls. Otherwise try typeclasses to generate 'good' default names..?https://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues/11Performance improvements2022-02-16T10:38:34ZIke MulderPerformance improvementsSome points where I think performance can still be improved:
- *`AsSolveGoal` TC search is slow.* this is now improved
- *Definitions like `IntroduceHyp` are not sealed off.* Seems to have no effect on performance though:
[with sealed...Some points where I think performance can still be improved:
- *`AsSolveGoal` TC search is slow.* this is now improved
- *Definitions like `IntroduceHyp` are not sealed off.* Seems to have no effect on performance though:
[with sealed definitions](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170877) vs [without sealed definitions](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170827).
- Stripping `□` of persistent hypothesis on introduction is slow?
- *Dedicated typeclass for `∀.. (tt: TT), ...`* Has no effect on performance:
[with dedicated typeclass](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170928) vs [without dedicated typeclass](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170827). But TC search debug output is more readable.
Continued: in the end there was a (small) performance improvement, just a bit later: [this](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170937) vs [this](https://gitlab.mpi-sws.org/iris/automation/-/jobs/170941). But quite possibly this was due to `rewrite /term` being slower than `unfold term`.https://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues/10Specifications with dependent existententials cannot be applied2021-09-08T17:41:56ZIke MulderSpecifications with dependent existententials cannot be appliedWhen we make an instance like:
```
Global Program Instance clone_arc_spec' γ (v : val) :
SPEC ∃ P HP, {{ is_arc P (HP := HP) γ v ∗ token P γ }}
clone v
{{ RET #(); token P γ ∗ token P γ }}.
```
where `HP : Fractional P`, the TC s...When we make an instance like:
```
Global Program Instance clone_arc_spec' γ (v : val) :
SPEC ∃ P HP, {{ is_arc P (HP := HP) γ v ∗ token P γ }}
clone v
{{ RET #(); token P γ ∗ token P γ }}.
```
where `HP : Fractional P`, the TC search for `FromTExist` fails, so the specification cannot be used.
It works fine if we leave `P` as an evar.https://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues/9Replace FindLocalUpdate with something better2021-06-25T08:18:09ZIke MulderReplace FindLocalUpdate with something betterIt would be nice if we can get some stronger guarantees when performing an update from `•a·○b` to `•a'·○b'`.
Right now `FindLocalUpdate` does not attempt anything of that sort: it takes the `○b` as an additional input to compute the `○b'...It would be nice if we can get some stronger guarantees when performing an update from `•a·○b` to `•a'·○b'`.
Right now `FindLocalUpdate` does not attempt anything of that sort: it takes the `○b` as an additional input to compute the `○b'` from. However, it should be possible to compute a `○b` that is minimal in some way! Some scratches of attempts:
```
Class CmraBiAbd {A : cmra} (x x' y y' : A) (φ : Prop) := {
cmra_biabd_valid : φ → x ⋅ y ~~> x' ⋅ y';
(* y is the minimum or there is no minimum *)
cmra_biabd_req_1 : φ → ∀ z z', x ⋅ z ~~> x' ⋅ z' → ((z ≼ y → y ≼ z) ∨ ∃ k k', k ≼ z ∧ x ⋅ k ~~> x ⋅ k');
(* y' is the maximum for y *)
cmra_biabd_req_2 : φ → x ⋅ y ~~> x' ⋅ y' → ∀ z', x ⋅ y ~~> x' ⋅ z' → y' ≼ z' → z' ≼ y';
}.
(* not sure if cmra_biabd_req_2 is provable, but the first two we can prove for the following lemma: *)
Lemma auth_subtract_l {A : ucmra} (x y r : A) φ :
UcmraSubtract y x φ r →
CmraBiAbd (● x) (● y) ε (◯ r) (φ ∧ ✓ y).
Proof.
```https://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues/7Typeclasses for simplifying ✓2021-06-23T09:40:51ZIke MulderTypeclasses for simplifying ✓It would be nice to have a typeclass which simplifies ✓ x for x in a given RA into its most basic representation.
- Should this live in BI..?It would be nice to have a typeclass which simplifies ✓ x for x in a given RA into its most basic representation.
- Should this live in BI..?https://gitlab.rts.mpi-sws.org/iris/diaframe/-/issues/5Remove & replace older experiments2022-02-11T15:53:53ZIke MulderRemove & replace older experiments- [x] Replace `delay_choice.made_choice` with some dedicated `DestructHint` type or similar.
- [x] Change `ReductionStep`s to no longer rely on lists: we don't use that anymore.
- [ ] Remove `proofstep` stuff?- [x] Replace `delay_choice.made_choice` with some dedicated `DestructHint` type or similar.
- [x] Change `ReductionStep`s to no longer rely on lists: we don't use that anymore.
- [ ] Remove `proofstep` stuff?