LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
283 stars 35 forks source link

Compilation issue with yojson 2.x.x #159

Open SnarkBoojum opened 2 years ago

SnarkBoojum commented 2 years ago

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.

xgqt commented 1 year ago

I just ran into this issue on Gentoo.

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

SnarkBoojum commented 1 year ago

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 commented 1 year ago

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

SnarkBoojum commented 1 year ago

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
gares commented 1 year ago

some output is different so it breaks some tests

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

SnarkBoojum commented 1 year ago

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 } ],
gares commented 1 year ago

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

gares commented 1 year ago

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

SnarkBoojum commented 1 year ago

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

SnarkBoojum commented 1 year ago

I added a commit to tighten the dependency on atd.