Mentions légales du service

Skip to content
Snippets Groups Projects
Select Git revision
  • develop default protected
1 result
user avatar
Front matter updated before archiving.
Julien Wintz authored
7a66e166
History
user avatar 7a66e166
History
Name Last commit Last update
.vscode
assets
media
mockups
src
.eslintrc.js
.gitignore
README.md
package-lock.json
package.json
tsconfig.json
README.md

This repository is now archived. Ongoig development happens here: https://github.com/LPCIC/elpi-lang.

Elpi Tracer - An tracer for ELPI: the Embeddable λ Prolog Interpreter

Original ADT document: ELPI.pdf

Getting up n' running

  1. Install & Setup OPAM
$ brew install opam # https://opam.ocaml.org/doc/Install.html
$ opam init
$ opam switch create 4.09.1
  1. Install & Setup Elpi/Elpi-Coq
$ eval $(opam env)
$ opam install elpi.1.15.2
$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam install coq-elpi.1.14.0
  1. Install & Setup VSCode
Install extension coq-elpi-lang

Use Case: Raw Elpi (https://github.com/gares/mlws18/blob/master/slides.pdf)

  1. Open tests/sources/w.elpi in VSCode (from elpi source code repository clone)
  2. Toggle terminal & run elpi
$ eval $(opam env)
$ elpi tests/sources/w.elpi
goal> main.

Use Case: Elpi W/ Coq

  1. Open examples/example_reflexive_tactic.v in VSCode (from coq-elpi source code repository clone)
  2. Click on line 234 "intros."
  3. VSCode Command: coq: interpret to point
  4. Move down one line
  5. VSCode Command: coq: interpret to point
  6. Move up one line
  7. Add "Elpi Trace."
  8. VSCode Command: coq: interpret to point
  9. Move down to monoid 0 Z.add. (a tactic implemented in elpi)
  10. VSCode Command: coq: interpret to point
  11. Navigate the trace in the dedicated window/panel, so far, it ends up in the output panel.

Provide the path $HOME/.opam/default/bin, depending on your host configuration.

Screenshot

Objective: The tracer

  1. In elpi source code repository clone, switch to the trace-browser branch
$ git checkout trace-browser
  1. Build this branch
$ eval $(opam env)
$ opam install atdgen
$ opam install atdts
$ opam install ./elpi.opam --deps-only --with-test
$ make build
$ atdts trace.atd
$ dune exec elpi -- -test -no-tc -trace-on json /tmp/foo.json -trace-at run 1 999 -trace-only user tests/sources/trace.elpi
$ cat /tmp/foo.json | dune exec elpi-trace-elaborator | ydump > /tmp/trace.json

Running the extension

So far, the extension is only a PoC at displaying the trace obtained in /tmp/trace.json in a VSCode panel. No connection with the rest of the software stack is immplemented so far.

  • Open this example in VS Code 1.49+
  • npm install
  • npm run watch or npm run compile
  • F5 to start debugging
  • In the panel, find the Elpi Tracer view
  • The run button computes and displays the trace navigator

**Relevant test files so far **

  • [elpi]/tests/sources/trace.elpi
  • [elpi]/tests/sources/trace2.elpi
  • [elpi]/tests/sources/trace_chr.elpi
  • [elpi]/tests/sources/trace_findall.elpi
  • [elpi]/tests/sources/trace_cut.elpi

These are checked when they do not break up the partial current implementation

Screenshot

Known issues

  • trace2.json: (0|6): In case of context location, rendering is messed up.
  • showMessage: Clear the breadcrumb based on a decent heuristic
  • switchTo: Make sure the breadcrumb switch happens by extending guards and keeping the navigation stack consistent
  • switch anyways not handled correctly in all cases
  • switchTo, jump: ensure the goal to index map is consistent
  • CUT card not formatted correctly
  • hopTo: When watching for a generated trace, whenever the transitional file changes, the trace is updated, which includes file locations, of course. If the elpi source file from which the trace originates is not the current buffer in VSCode, file location links do not work.
    • Add safe guards at the least
    • Either the trace keeps tracks of the original elpi/elpi-coq source file
    • Either assumptions should be made
      • ?
      • ?
    • Fix toggling of subruntimes after ignoring Init cards.

Remarks

Ticked when discussed. Either dismissed or turned into a task.

  • Now that goal_text is displayed as formatted code, one dearly wants to click on it to visually match the corresponding source file
    • Shouldn't a rule keep track of the file location it originates from ?
    • Could be computed upwards from the bottom of the various stacks, but would it make sense ?
    • Would end up being a location tag on the top right corner of a selected card RHS rendering
    • Reflected in the attempts, my bad

TODO

  • Refactor internal mapping to ensure correct goal references
    • Get rid of the goal to index map
    • Use tuples or multiple maps
    • Ensure consistency and uniqueness when probing index <-> (runtime_id, step_id, goal_id)
    • Validate all examples
    • Towards unit testing ?
    • Formatting stack may be impacted
  • Code fragments syntax coloring - best option seems to use shiki and link vs code variables in shiki's css-variables them, believe it or not, vscode provides no API over its syntax highlighting engine.
  • Successful attempts, some file locations remain displayed, just before the rule rendering refactoring
  • Add a clear button to the trace inspector panel
  • Auto clear the contents on subsequents runs
  • Implement the corresponding logic
  • Add a badge in the RHS view to remind the couple (rt,st)
  • Architecture REdesign: For what comes next:
    • Integrate the atd generated typesecript API parser
    • Update RHS CARD PANEL TEMPLATE to be chosen in a list of templates depending on the rule kind|type
    • format_rule -> format_XXX_rule
    • At this point, all examples should render exhaustively and without error
  • CARD FOR GOAL Handle the case of an INIT step kind|type
  • CARD FOR GOAL Handle the case of an FINDALL step kind|type
    • This implies parsing the 'findall' fields as well
    • And child cards for incremented runtime id
    • Display them indented under their parent card in a collapsible way
  • CARD FOR GOAL Handle the case of a SUSPEND step kind|type
    • To be tested further
  • CARD FOR GOAL Handle the case of a CUT step kind|type
    • To be tested further
  • CARD FOR GOAL Handle the case of a RESUME step kind|type
    • To be tested further
  • CARD FOR GOAL Handle the case of a CHR step kind|type
    • New panel for Store before
    • New panel for Store after
  • Parse subsequent runtimes CHR & FINDALL Cases
  • CARD for GOAL (LHS):
    • In case of a yellow status display a list of more successful attempts next to the badge (these are step ids in the same runtime)
  • CARD for GOAL (LHS):
    • The status field should be the footer of the card, made sexy in whatever manner
  • CARD for GOAL (RHS):
    • In case of an empty panel (e.g. Failed attempts of an inference rule with no entries), add a tiny footer that honors the corner radius of the overall element and makes otherwise visually clear it is empty.
  • LHS Card Feed:
    • When two runtimes are forked from a step representend by a card: add a dividider between sub runtime ids to easily identify them
  • STACK:
    • No more dividers
    • One line per rule
    • Rule text is displayed on the left and links to the card of corresponding goal
    • Add a button on the right to jump to the corresponding location on the right whenever applicable
    • Add a badge with the rule's (r_id|s_id) tuple
    • Keep the rule "kind" badge -> as tooltip
  • PANEL for GOAL (RHS):
    • In case of a yellow status display a new section: MORE SUCCESSFUL ATTEMPTS that contains the very same list, with hyperlinks of course
    • Sibling tag to be colored with status of destination goal
  • ELPI ELABORATOR/TRACER PANEL header improved:
    • If embeded inside the view, move navigation controls within
    • Add a field displaying the source file for which the trace has been computed
    • Add an editable field to override default CL arguments:
      • e.g. -test: This one for sure
      • retrieve and use its value
      • e.g. --options: 0 999 > /tmp/... should be hidden and somehow acceptable for any run (mentionned for the record) - TO DISCUSS
  • COQ-Elpi link: WATCHING feature
    • This ends up creating new commands, with corresponding (icon) entries in the panel header
    • Start watching: elpi.watch_start Sets up a filesystem watcher on the conventionally chosen destination for the trace generated by elpi in the coq context
    • Stop watching: elpi.watch_stop Kills this file system watcher
    • Make sure these commands can be invoked by another extension - by design
    • VISUALS: Add a spinning icon or whatever when the watcher is running
  • Propose a design or heurstics so that LHS & RHS folding for subcards gets intuitive and (semi ?) automatic
    • Link toggles between LHS, RHS
  • Goal jumping: Keep the current design but ensure the destination has minimal step id within the smae origin runtime in case of multiple destinations with same id - TO BE DISCUSSED FURTHER
  • Reduce before & after margins for subgoals rendering in successful attempts
  • Add a glyphish font dependency
  • Add a header for navigation (Back|Forward buttons) & Card filtering
  • Implement navigation logic stack based on message shows
  • Implement filtering logic stack based field inputsibling goal if it currently filtered ?
  • Get rid of faker.js
  • Deal with bulma-extensions
    • For tooltips
    • For dividers
  • VISUALS: make each hand side individually scrollable!
  • VISUALS: Fix mdi font usage and disseminate glyphs
  • Add an ergonomic animated scrolling module to reflect the navigation in the trace
  • Pass parsed JSON trace to the view
  • Implement card rendering
    • Fix heuristics for color codes status: a new field has been added in the trace type definition
  • Implement step rendering
    • Set all element ids as data attributes whenever available
    • Implement hyperlinks (that is link goal ids)
    • Feedback API to open file & switch to place - That is a message from the view (js) back to the provider controller (ts)
    • Beautify it all
  • Source code beautifying WRT/ relevant practices & standards
  • Use a better alternative for the child-process node module
  • Match VSCode theme in extensions css styles
    • Beautify that
  • Design the settings for this extension
    • Investigate the link with ocaml-platform VSCode extension
    • Introspect opam environment
    • Infer binaries location
      • dune
      • elpi
      • elpi-trace-elaborator
  • Continuous manual testing on macOS
  • Continuous manual testing on Linux
  • Continuous manual testing on Windows
  • Use minified versions of dependencies to decrease extension load time
  • Extension publication facility
  • CI facility to update, build & publish the (sphinx based) documentation
    • Fork elpi repository on gitlab for a start
    • Happens in the trace-browser feature/doc branch forked from master
    • RST documentation files include examples
    • These examples are to be run and the results (stdout output) to be injected in the documentation during the generation step
    • Maybe use github:cop/doc/tools/coqrst as a starting point for inspiration kept things much simpler for the moment
    • Rename elpi:feature/ghpages to elpi:feature/doc
    • Merge elpi:trace-browser back into elpi:feature/doc
    • Inject dune build $(DUNE_OPTS) @doc somehow
    • CI gh-pages setup
  • Test status heuristics on many more examples, after subsequent fixes in elpi:trace-browser

References