loadLemmaLibrary and loadLemmaLibraryWith not working

[roboguy13]

It looks like either the client isn't parsing the result from the server correctly here or the server isn't sending the result in the right format (or both).

Running hermit-shell Century.hs in examples/reasoning-paper/MakingACentury:

HERMIT> eval "rule-to-lemma 6.2"
6.2 (Not Proven)
  filter ▲ ((.) ▲ ▲ ▲ good value)
  ≡
  (.) ▲ ▲ ▲ (filter ▲ ((.) ▲ ▲ ▲ good value))
      (filter ▲ ((.) ▲ ▲ ▲ ok value))
[Done]

HERMIT> proveLemma "6.2"
Goal:
  filter ▲ ((.) ▲ ▲ ▲ good value)
  ≡
  (.) ▲ ▲ ▲ (filter ▲ ((.) ▲ ▲ ▲ good value))
      (filter ▲ ((.) ▲ ▲ ▲ ok value))
[Done]

HERMIT> query $ loadLemmaLibrary "HERMIT.Libraries.Int.lemmas"
parsed fine
*** Exception: failed to parse result value for query (loadLemmaLibrary  HERMIT.Libraries.Int.lemmas): Object (fromList [("result",String "Successfully loaded library HERMIT.Libraries.Int.lemmas\n"),("output",Array (fromList [Array (fromList [Object (fromList [("text",String "'\"Object (fromList [(\\\"params\\\",Array (fromList [Object (fromList [(\\\"params\\\",Array (fromList [String \\\"HERMIT.Libraries.Int.lemmas\\\",Null])),(\\\"method\\\",String \\\"loadLemmaLibrary\\\")])])),(\\\"method\\\",String \\\"query\\\")])\" [correct]\n")])])]))]) : malformed Object returned from Server
HERMIT> 
HERMIT> query $ loadLemmaLibraryWith "HERMIT.Libraries.Int.lemmas" "LteFalseImpliesEqFalseInt"
*** Exception: failed to parse result value for query (loadLemmaLibrary LteFalseImpliesEqFalseInt HERMIT.Libraries.Int.lemmas): Object (fromList [("result",String "Successfully loaded library HERMIT.Libraries.Int.lemmas\n"),("output",Array (fromList [Array (fromList [Object (fromList [("text",String "'\"Object (fromList [(\\\"params\\\",Array (fromList [Object (fromList [(\\\"params\\\",Array (fromList [String \\\"HERMIT.Libraries.Int.lemmas\\\",String \\\"LteFalseImpliesEqFalseInt\\\"])),(\\\"method\\\",String \\\"loadLemmaLibrary\\\")])])),(\\\"method\\\",String \\\"query\\\")])\" [correct]\n")])])]))]) : malformed Object returned from Server
HERMIT> 

[ecaustin]

Sorry, I just saw this.

Given that you see the the debug message "parsed fine," I'm going to assume that this is related to the work I was doing with binding return values of queries (I left that print statement in on my last checkin apparently).

It looks like the return value is being returned, but its JSON representation isn't parsing correctly for some reason.

I've got my fingers crossed this will be fixed by the work @andygill is doing this week, otherwise I'll take a look at this first thing when I get back in town.

[roboguy13]

Here's what that same example looks like with the current debugging info:

HERMIT> eval "rule-to-lemma 6.2"
6.2 (Not Proven)
  filter ▲ ((.) ▲ ▲ ▲ good value)
  ≡
  (.) ▲ ▲ ▲ (filter ▲ ((.) ▲ ▲ ▲ good value))
      (filter ▲ ((.) ▲ ▲ ▲ ok value))
[Done]

HERMIT> proveLemma "6.2"
Goal:
  filter ▲ ((.) ▲ ▲ ▲ good value)
  ≡
  (.) ▲ ▲ ▲ (filter ▲ ((.) ▲ ▲ ▲ good value))
      (filter ▲ ((.) ▲ ▲ ▲ ok value))
[Done]

HERMIT> query $ loadLemmaLibrary "HERMIT.Libraries.Int.lemmas"
Internal Error: Parser Failed
{
    "params": [
        {
            "params": [
                "HERMIT.Libraries.Int.lemmas",
                null
            ],
            "method": "loadLemmaLibrary"
        }
    ],
    "method": "query"
}
*** Exception: failed to parse result value for query (loadLemmaLibrary  HERMIT.Libraries.Int.lemmas): Object (fromList [("failure",String "internal error")]) : internal error
HERMIT> query $ loadLemmaLibraryWith "HERMIT.Libraries.Int.lemmas" "LteFalseImpliesEqFalseInt"
Internal Error: Parser Failed
{
    "params": [
        {
            "params": [
                "HERMIT.Libraries.Int.lemmas",
                "LteFalseImpliesEqFalseInt"
            ],
            "method": "loadLemmaLibrary"
        }
    ],
    "method": "query"
}
*** Exception: failed to parse result value for query (loadLemmaLibrary LteFalseImpliesEqFalseInt HERMIT.Libraries.Int.lemmas): Object (fromList [("failure",String "internal error")]) : internal error

[ecaustin]

Commit https://github.com/ku-fpg/hermit-shell/commit/bc25391a9cdd66ab893259bd75a9e151a3158006 is a partial fix.

We didn't have an external instance for query that handled non-unit returns, so I added one for String values matching the return type of loadLemmaLibrary. Now you should get an exception like:

HERMIT> query $ loadLemmaLibrary "HERMIT.Libraries.Int.lemmas"
*** Exception: failed to parse result value for query (loadLemmaLibrary  HERMIT.Libraries.Int.lemmas): Object (fromList [("result",String "Successfully loaded library HERMIT.Libraries.Int.lemmas\n"),("output",Array (fromList [Array (fromList [Object (fromList [("text",String "Successfully loaded library HERMIT.Libraries.Int.lemmas\n\n")])])]))]) : malformed Object returned from Server

I have no idea why that object is malformed, it seems to conform to our definition of parseJSON for ShellResult values.

[roboguy13]

So, I figured out what the issue is. query' is the new query function that returns a real value while the other one has the type query :: Guts a => Transform a b -> Shell (). As a result, the () type was being picked instead of the String type, giving a parse error.

I just pushed bc25391, which added the ability to get a String response.

The issue now is that the message is getting printed on the server side before it gets sent back over, which is not what we want. That's also why I used print instead of putStrLn in instance Response String, so that we can see that the second message is a String being printed on the client side.

[roboguy13]

There's also the deeper issue of whether or not this is what we want to return from loadLemmaLibrary in the first place (I'm thinking no).

[ecaustin]

Doh. Yup, I totally forgot to switch to query' after I fixed the missing query external. In fact, now that this is working, we can probably just make query' the only query command since the () Response instance mimics the old behavior.

As for the return type of loadLemmaLibrary, I believe the intention was to provide a success message separate from the other output messages. I have no idea why that decision was made, though, and would be fine appending it the current return string to the tail of the other glyphs and just using a () return type.

[xich]

It returned a string because this is how things were printed in the old shell. Anything that returned a string was treated specially, and the string was printed back to the user. (Strictly speaking, even though rewrites have access to IO, they shouldn't call print or putStrLn directly.) So if the new shell has some other way to send back success/failure messages to the user, then feel free to change things.