Paul F. Dietz (863a4b0f) at 31 Mar 14:55

If necessary, for future patches, let's leave this on a branch for now. I'll edit the .qlfile in spec-map-docker.

Ping Paul R. when this is ready to merge.

Paul F. Dietz (7e6479a9) at 21 May 18:27

... and 32 more commits

Paul F. Dietz (351302ad) at 21 May 18:27

... and 38 more commits

Should confirm (assert?) that traces is non-null.

(Resolve and merge when you feel this is addressed.)

Most of this commit is made up of test files.

In the rest, we:

• Remove the internal protocol definitions
• Add parsers for TAP and xUnit, the most common test output formats
• Add the ability to extract and run test cases in googletest format
• Add the ability to extract individual conditions from test cases
• Add the ability to extract examples from (suitable) individual test conditions

To answer my question: html-entities

I created an issue for that.

https://git.grammatech.com/synthesis/sel/-/issues/108

I put in a few comments. A general comment: add many more docstrings and :documentation strings.

SEL has a function like this. They should be unified. Also, I have seen cases where .h files are actually C++; this would require attempting to parse with the C grammar and getting errors, then trying CPP (or, grepping for things like class or namespace).

I don't understand this TODO comment - is this code too slow, or is create-software too slow?

Aside: is there a CL library for removing/adding these &...; escapes in strings? I could have used this recently.

Idle thought: I'm wondering how well this parses. If poorly, can we inform the parser what certain macros mean, short of expanding everything?

Most of this MR is made up of lens definitions and their tests. Since both of the languages we are translating to (Tyrell, which is used by Trinity, and FPCore, which is used by Herbie) are sexp-based, as is SMT-LIB which I believe will be the next lens added, I’ve taken a two-stage approach, first translating Python into a generic s-expression format and then translating that into the specific languages we need.

You may need to update Quicklisp/Serapeum, since many of the lens definitions rely on serapeum:make being defined as a pattern, which was added recently.

The MR also adds the actual Herbie muse, using the FPCore lens, and two integration tests for it.

While testing Herbie I ran into problems with how we send changes to the client. The MR also fixes that, by changing the way we call out to diff: basically we now take advantage of diff’s ability to output changes as an ed(1) script and translate that directly into LSP edits.

Changing how diffing works meant several integration tests were now invalid. Rather than re-record them I edited them by hand.

Eric dinged me for reading a file to create a sw object, and said I should use create-software instead. Should create-software also be used to read from strings?

:documentation for the define-package form?