RefinedC issueshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues2021-04-28T17:50:30Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues/36Add idtac; in front of all tactics2021-04-28T17:50:30ZMichael SammlerAdd idtac; in front of all tacticsAdding `idtac;` in front of all tactics helps the Ltac profiler as it is otherwise confused by expression evaluation time and tactic running time. Also it should make the names in the profiler acurate. This tip comes from Jason Gross.Adding `idtac;` in front of all tactics helps the Ltac profiler as it is otherwise confused by expression evaluation time and tactic running time. Also it should make the names in the profiler acurate. This tip comes from Jason Gross.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues/23Improve performance of typeclass search2020-11-23T07:50:17ZMichael SammlerImprove performance of typeclass searchIdeas:
- [ ] Figure out how much time we spend on typeclass search
- [ ] Try using a custom DB with the discriminated option and [Hint Variables Opaque](https://coq.inria.fr/refman/proof-engine/tactics.html#coq:cmdv.hint-variables) and f...Ideas:
- [ ] Figure out how much time we spend on typeclass search
- [ ] Try using a custom DB with the discriminated option and [Hint Variables Opaque](https://coq.inria.fr/refman/proof-engine/tactics.html#coq:cmdv.hint-variables) and friends
- Downside: There is no Global Hint Resolve
- [ ] Try making `rty_type` a parameter of `rtype` instead of part of the sigma type (e.g. `int` would be `rtype Z`
- This hopefully would allow making `int` and other `rtype` typeclasses opaque
- [ ] Try [Set Filtered Unification](https://coq.inria.fr/refman/addendum/type-classes.html#coq:flag.typeclasses-filtered-unification)
- Probably too strong, as it applies to all hint databaseshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/issues/22Better performance measurement infrastructure2020-10-25T09:43:40ZMichael SammlerBetter performance measurement infrastructureIt would be great to have a more fine-grained breakdown of the performance of verification.
Ideas:
- [ ] Add `Time` and `Set Ltac Profiling` around the different parts of function verification and have them automatically be inserted by ...It would be great to have a more fine-grained breakdown of the performance of verification.
Ideas:
- [ ] Add `Time` and `Set Ltac Profiling` around the different parts of function verification and have them automatically be inserted by a flag to the frontend
- [ ] Have a script to automatically compare the output between different commits
- [ ] Integrate more information with http://coq-speed.mpi-sws.org/
- Not sure how since the only reliable number is instruction count, not time, see e.g. [this diff](http://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=time&var-project=refinedc&var-branch=master&var-config=All&var-group=().*&from=1600297747422&to=1601174726441)
- Can one somehow send signals to perf?