back to root

back to Zipperposition

cleaning Zip

• Petar Vukmirovic

  2019-11-13 13:43:42 (GMT)

  Hi all,

• Petar Vukmirovic

  2019-11-13 13:43:51 (GMT)

  I have some time to clean Zip finally.

• Petar Vukmirovic

  2019-11-13 13:44:8 (GMT)

  Should we make some plan of what should be done before releasing 1.6?

• Simon Cruanes

  2019-11-13 15:23:20 (GMT)

  Sure. It's only cleaning, right? no new feature.

• Simon Cruanes

  2019-11-13 15:32:16 (GMT)

  We can discuss that more on a call today, if you want.

• Petar Vukmirovic

  2019-11-13 16:25:29 (GMT)

  Absolutely

• Petar Vukmirovic

  2019-11-13 16:25:38 (GMT)

  Just let me know when you have the time

• Simon Cruanes

  2019-11-13 16:54:50 (GMT)

  Plan

  Invariants to preserve in each PR

  • unit tests must pass
  • ensure travis is green before merging (do PRs)
  • try a small-ish run on TPTP (soundness check)

  Things to do:

  • make all options non-global
    • carry Flex_state.t around and give it to Cnf, etc. instead of global options
  • use UnifFramework everywhere in HO, remove PragHOUnif
  • document UnifFramwork.PARAMETERS (or point to arxiv paper in readme)
  • turn PragUnifParams into a bunch of flexstate keys
  • run ocp-indent before merging
  • perf: regression testing on FO
    • compare to previous CASC results?
    • check on examples/ incl. pelletier problems
    • check that AVATAR still works well (with msat 0.8)