lpcic / elpi-lang Goto Github PK

I think it would be cleaner to have a watch mode without the fields to pass options, and a run mode with options but no watch buttons

currently we use colors to immediately visualize if a sibling worked or not.

sometimes it does not display the trace, but opening it again by hand works

I've a trace where goals are "undefined",

trace.zip

But actually, I believe the trace is not special, since even trivial examples have the same bug. Hence I suspect it is related to my setup. This is VSCode

Version: 1.74.3
Commit: 97dec172d3256f8ca4bfb2143f3f76b503ca0534
Date: 2023-01-09T16:57:40.428Z
Electron: 19.1.8
Chromium: 102.0.5005.167
Node.js: 16.14.2
V8: 10.2.154.15-electron.0
OS: Linux x64 5.15.0-56-generic snap
Sandboxed: No

CC @jwintz

Loading this trace (vscode 1.72) takes forever. In particular a few seconds before the UI shows the card, then a few second before each card shows up its goal text. The third card text is "Cut", and it still takes time for it to appear.

If I had to point the finger, it would be syntax highlighting code. Is there an easy way to disable it, so that I can validate or refuse this thesis?

trace-qui-rame.js.gz

CC @jwintz

How to detect the problem:
type in an Elpi file a word containing internally the substring pi (or sigma), such as
typing and see the colouration of the "pi".

Notice that this problem often breaks the syntax detection of the rest of the file.

Whenever I have to debug a program failing at some point without an error, I like to scroll to the bottom of the goal list, to see what the last goal it attempted was. However, the scrollbar starts hidden behind the top and bottom bar, the navigation history bar and the goal filter bar. In the picture below I scrolled up a bit from the bottom such that you can see where the scroll bar is.

To scroll quickly I drag the scroll bar to the bottom but I can't as long it is hidden. Thus I have to scroll manually till I see the scroll bar. When I have a lot of goals that sometimes takes a bit.

The trace visualisation and navigation has been merged into a candidate branch for the next release.

Before requesting a merge into master, subsequent developments will happen here.

This issue will help track issues and tasks remaining when archiving the proof of concept original repository.

NOTE: Syntax highlighting tested and working fine with no regression.

Issues

• 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
    • ?
    • ?

TODO

• 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.
  • Format *_text exhaustively
• Propose a design or heurstics so that LHS & RHS folding for subcards gets intuitive and (semi ?) automatic
  • Link toggles between LHS, RHS
• Design the settings for this extension
  • Investigate the link with ocaml-platform VSCode extension Doesn't build at the moment of writing
  • Settings contribution point: declare and retrieve
  • Binaries location
    • elpi
    • elpi-trace-elaborator
• M$ Windows compatibility & testing, use node process piping for that
• Illustrate README.md with screenshots and screencasts
• Publication facility

no need to use vscode

currently does not work

trace.tmp.json.zip