☂️ Gillian 1.0

[giltho]

This serves as a megathread for issues to be fixed for "Gillian 1.0", whenever that may be.

• Core functionality / bugs

  • Gillian-JS is broken #113
  • Properly handle branch cmds with only one outcome #151
  • Make GIL lists actually look like lists #152
  • Rewrite the reduction loop  #162
  • Import Kanillian and its memory model #164
  • Have specifications in a separate file #166
  • Make "failed to create UP" errors more informative #174
  • Match the theory: the engine should allow branching with error and successes #182
  • Render file log to HTML #211

• Cleanup

  • Seperate the Engine from the FOSolver #4
  • Split CommandLine.ml into multiple files #126
  • Refactor excessively long functions into modules #127
  • Fix Gillian's Infra #131
  • Rewrite over-abbreviated type aliases #140
  • Definitively decide between _opt and _exn funcs #144
  • Split the Asrt type #159
  • Check for unused config flags and remove previously_normalised #179
  • Get rid of alcotest-runner #191
  • Rename Unification to Matching #196
  • Get rid of old parallel code #204
  • GIL should have a sane syntax #236

• Documentation

  • Add README for debugger #123
  • Remove unnecessary @inlines (when an odoc bug is fixed) #198
  • Cover all public-facing modules in documentation #199
  • Write quick style guidelines #200

• Performance

  • Types modeled as strings should be opaque #7
  • Actions should have an opaque type instead of string. #8
  • Evaluate and improve logging performance #146
  • Revert use of visitors for substitution #163
  • Make monadic more efficient #178

• Debugger / Lifter

  • Lift states #145
  • "Replay" commands with TMI logging #147
  • Extend the debugger to handle more execution contexts #148
  • Visualise heaps #149
  • Make lvars look nicer in debugger interface #153
  • Enhance unify map #170
  • Check if breakpoints still work #171
  • WISL debugging: bug when while after branch #175
  • Add show/hide button for ExecMap/UnifyMap expansions #176
  • Add a note to debugger UI when debugger terminates/disconnects #181
  • Add breakpoint marker to ExecMap #194
  • Gil_fallback_lifter: Defer skipping behaviour to TL lifter #201
  • Show what's been consumed in the state during unification #220

• Old objectives
  Original issue reads:
  This is the umbrella issue for putting the Gillian implementation back on track.
  With all the projects and experiments being conducted as well as preparing the artifacts, the project is a bit unstable, CI is not passing and there are broken features and disabled tests.

  • reestablish incremental verification #78
  • Debugger merging #86
  • Split CommandLine.ml into multiple files #126
  • Fix Test262 (covered by Gillian-JS is broken #113; Test262 has already been fixed)
  • Fix the entire CI - fixed in Update ci and disabled JS tests #184

[giltho]

@nat rename this as "Gillian 1.0" and write a proper checklist

[NatKarmios]

Okay, done, this is a bit of a megathread on issues now.

[NatKarmios]

@giltho feel free to elaborate on / prune some of these when you get the time