cabal repl saw fails if cabal build isn't run beforehand

[RyanGlScott]

From a clean git clone of saw-script, running cabal repl saw fails:

$ cabal repl saw
Build profile: -w ghc-8.10.3 -O1
In order, the following will be built (use -v for more details):
 - saw-script-0.7.0.99 (first run)
Preprocessing library for saw-script-0.7.0.99..
Building library for saw-script-0.7.0.99..
<elided>
Preprocessing executable 'saw' for saw-script-0.7.0.99..
setup: can't find source for GitRev in saw,
/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/dist-newstyle/build/x86_64-linux/ghc-8.10.3/saw-script-0.7.0.99/build/saw/autogen,
/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/dist-newstyle/build/x86_64-linux/ghc-8.10.3/saw-script-0.7.0.99/build/global-autogen

cabal: repl failed for saw-script-0.7.0.99.

Curiously, this doesn't occur if cabal build is ran before cabal repl saw.

[RyanGlScott]

Ah, this is because saw-script uses a custom Setup script! In particular, this script overrides the build hook but not the repl hook, which explains the discrepancy above.

Looking at this script more closely, however, all it appears to do is compute the git hash. Would it not be cleaner to use a Template Haskell–based solution like the gitrev library? This is what cryptol does, for instance.

[atomb]

IIRC, the Template Haskell approach didn't work because some of the code from the saw executable can't be loaded into GHCi (which Template Haskell uses for evalutation). But of course that's exactly what you're trying to do. :) The issue there is that we link with a large C/C++ library, abc, which GHCi tries to load when it starts up. GHCi's object file loader is custom code which segfaults on this particular library. We'll be removing the library dependency before long, which should address this problem, but for the moment it won't work.

For the moment, loading just the saw-script library, and not the saw executable, seems to work.

[RyanGlScott]

IIRC, the Template Haskell approach didn't work because some of the code from the saw executable can't be loaded into GHCi

Really? I'm able to load saw into GHCi with cabal repl just fine (after running cabal build).

[atomb]

Maybe GHCi is better now! :) Which version is this?

[atomb]

It fails for me with 8.6.5, which is one of the versions I'd like to continue supporting for a little while. Once 9.0.1 is out, I think dropping 8.6.5 might make sense.

[RyanGlScott]

Which version is this?

GHC 8.10.3 on Linux.

[atomb]

This also might be a macOS-specific problem, since object file formats are different on macOS and Linux. I'm currently testing 8.8.4 and then I'll try 8.10.3.

[RyanGlScott]

It fails for me with 8.6.5, which is one of the versions I'd like to continue supporting for a little while.

Interesting. I'm able to cabal repl saw with GHC 8.6.5 on Linux, so I wonder if this is a macOS bug or if I'm just lucky. What is the exact error you're getting, out of curiosity?

[atomb]

I get two different results for two different commands. Doing exactly what you did yields this:

$ cabal repl saw
Build profile: -w ghc-8.6.5 -O1
In order, the following will be built (use -v for more details):
 - saw-script-0.7.0.99 (file /Users/atomb/galois/saw-script/dist-newstyle/build/x86_64-osx/ghc-8.6.5/bv-sized-1.0.2/cache/build changed)
Preprocessing library for saw-script-0.7.0.99..
Building library for saw-script-0.7.0.99..
Preprocessing executable 'saw' for saw-script-0.7.0.99..
GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
ghc:
lookupSymbol failed in relocateSection (relocate external)
/Users/atomb/galois/saw-script/deps/abcBridge/abc-build/libabc.a: unknown symbol `___dso_handle'
ghc:
lookupSymbol failed in relocateSection (relocate external)
/Users/atomb/galois/saw-script/deps/abcBridge/abc-build/libabc.a: unknown symbol `___dso_handle'
ghc: unable to load package `abcBridge-0.17.1'
cabal: repl failed for saw-script-0.7.0.99.

Using exe:saw instead of saw yields this:

$ cabal repl exe:saw
Build profile: -w ghc-8.6.5 -O1
In order, the following will be built (use -v for more details):
 - saw-script-0.7.0.99 (file /Users/atomb/galois/saw-script/dist-newstyle/build/x86_64-osx/ghc-8.6.5/bv-sized-1.0.2/cache/build changed)
Preprocessing library for saw-script-0.7.0.99..
Building library for saw-script-0.7.0.99..
Preprocessing executable 'saw' for saw-script-0.7.0.99..
GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
cabal: repl failed for saw-script-0.7.0.99. The build process segfaulted (i.e.
SIGSEGV).

I've confirmed that the same happens with 8.8.4.

[RyanGlScott]

Thanks. I now see that cabal repl saw is advised against in the README, although it wasn't clear to me what the problem was (nor that it appears to be somewhat OS-dependent) until #1004 (comment).

In that case, I'll wait until the abcBridge dependency is removed (#975). Is that just waiting on #562? The description in #975 leads me to believe so, but #562 is closed, so I'm not entirely sure.

[atomb]

I also want to do a bit more performance testing before finalizing it, but it's otherwise ready.

[robdockins]

Maybe this can be resolved now that abc is no longer linked in?

[RyanGlScott]

Indeed. I wasn't able to reproduce the issue above since I don't use macOS. Could a macOS user try running cabal repl now to see what happens?

[RyanGlScott]

One addition challenge is that after #1908, saw-script's custom Setup.hs script doesn't just check the git hash of saw-script itself, but also several other libraries that saw-script depends on:

saw-script/Setup.hs

Lines 39 to 54 in 8561a21

	writeFile (dir </> "GitRev.hs") $ unlines
	[ "module GitRev where"
	, "-- | String describing the HEAD of saw-script at compile-time"
	, "hash :: String"
	, "hash = " ++ show desc
	, "-- | String describing the HEAD of the deps/aig submodule at compile-time"
	, "aigHash :: Maybe String"
	, "aigHash = " ++ show aig_desc
	, "-- | String describing the HEAD of the deps/what4 submodule at compile-time"
	, "what4Hash :: Maybe String"
	, "what4Hash = " ++ show w4_desc
	, "-- | String describing the most recent commit which modified the rme directory"
	, "-- at compile-time"
	, "rmeHash :: Maybe String"
	, "rmeHash = " ++ show rme_desc
	]

It's unclear to me if the gitrev API makes it possible to query the git hashes of library dependencies at compile time. If not, we may need to look into another library such as githash.