elpi icon indicating copy to clipboard operation
elpi copied to clipboard

Compilation issue with yojson 2.x.x

Open SnarkBoojum opened this issue 3 years ago • 10 comments

If one compiles a more recent yojson (2.0.2 here), then use it against ocaml-atd 2.9.1, then the resulting lib breaks elpi:

File "src/elpi_trace_elaborator.ml", line 668, characters 14-16:
668 |   write_trace ob cards;
                    ^^
Error: This expression has type Bi_outbuf.t
       but an expression was expected of type Buffer.t

because indeed in the 2.x.x series, yojson doesn't use biniou anymore, so Bi_outbuf isn't there anymore.

I noticed it because I'm looking into updating yojson in Debian, so I could find everything that breaks and report to the various upstreams.

I'll try to provide a patch.

SnarkBoojum avatar Aug 15 '22 13:08 SnarkBoojum

I just ran into this issue on Gentoo.

@SnarkBoojum have you had time to see if this can be patched?

xgqt avatar Oct 23 '22 09:10 xgqt

I have no clue where write_trace comes from... the three lines can probably replaced with something like List.map (fun card -> Yojson.Safe.to_channel stdout card) cards ; but first cards needs to be turned into Yojson.Safe.t and I don't know how.

SnarkBoojum avatar Oct 24 '22 08:10 SnarkBoojum

(now that I think of it, write_trace is probably from trace.atd)

SnarkBoojum avatar Oct 24 '22 08:10 SnarkBoojum

Here is a first draft ; some output is different so it breaks some tests, but it doesn't look insane:

--- elpi.orig/src/elpi_trace_elaborator.ml
+++ elpi/src/elpi_trace_elaborator.ml
@@ -664,6 +664,6 @@
 
   let cards = Trace.cards steps ~stack_frames ~aggregated_goal_success ~goal_text ~goal_attempts in
 
-  let ob = Bi_outbuf.create_channel_writer stdout in
-  write_trace ob cards;
-  Bi_outbuf.flush_channel_writer ob
+  let buf = Buffer.create 1000 in
+  write_trace buf cards;
+  Buffer.output_buffer stdout buf

SnarkBoojum avatar Oct 24 '22 09:10 SnarkBoojum

some output is different so it breaks some tests

how? (not that I did a release on Friday since the test suite was broken)

gares avatar Oct 24 '22 09:10 gares

Well, using a different yojson means pretty printing has some slight differences ; for example:

--- elpi.orig/tests/sources/trace.elab.json
+++ elpi/tests/sources/trace.elab.json
@@ -271,8 +271,7 @@
                 }
               ],
               "events": [
-                [ "Assign", "A0 := 1" ],
-                [ "Assign", "A1 := 2 + 3" ]
+                [ "Assign", "A0 := 1" ], [ "Assign", "A1 := 2 + 3" ]
               ]
             },
             "siblings": [ { "goal_text": "calc (2 + 3) 1", "goal_id": 8 } ],

SnarkBoojum avatar Oct 24 '22 09:10 SnarkBoojum

Oh, but this change is more about ydump than your patch. Maybe it has a flag to stick to the old format?

gares avatar Oct 24 '22 09:10 gares

(yojson prints a single line, I then run ydump on it to make the test reference readable)

gares avatar Oct 24 '22 09:10 gares

It's not backward-compatible ; in fact I'm using yojson 2.0.2 and atd 2.10.0.

SnarkBoojum avatar Oct 24 '22 11:10 SnarkBoojum

I added a commit to tighten the dependency on atd.

SnarkBoojum avatar Oct 25 '22 08:10 SnarkBoojum