GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-04 01:17:40 +03:00
Code Issues Projects Releases Wiki Activity

use file-embed to make TH file embedding more robust

Browse Source 
Haskell Language Server still struggles a bit with opening projects that
are subprojects of larger projects (in the git submodule sense).

When opening such projects from within their parent project, the overall
project path remains the outermost one, which breaks relative paths of
subprojects.

The file-embed has a utility to help with such path adjustments.
Theoretically, HLS will eventually support "multi-home units", where
different files will be compiled under different home folders if they
belong to subprojects, but in the meantime, this un-breaks HLS for users
that open Cryptol as a subproject of, say, SAW.
This commit is contained in:
Valentin Robert 2024-01-23 14:11:02 -08:00
parent 7ab8ca5820
commit e9c41586ea
2 changed files with 11 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cryptol.cabal
View File

@ -58,11 +58,11 @@ library
deepseq >= 1.3,
directory >= 1.2.2.0,
exceptions,
file-embed >= 0.0.16,
filepath >= 1.3,
gitrev >= 1.0,
ghc-prim,
GraphSCC >= 1.0.4,
heredoc >= 0.2,
language-c99,
language-c99-simple,
libBF >= 0.6 && < 0.7,

22
src/Cryptol/Prelude.hs
View File

@ -8,10 +8,9 @@
--
-- Compile the prelude into the executable as a last resort
{-# LANGUAGE Safe #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Cryptol.Prelude
( preludeContents
@ -23,28 +22,27 @@ module Cryptol.Prelude
, cryptolTcContents
) where
import Data.ByteString(ByteString)
import Data.ByteString (ByteString)
import Data.FileEmbed (embedFileRelative)
import qualified Data.ByteString.Char8 as B
import Text.Heredoc (there)
preludeContents :: ByteString
preludeContents = B.pack [there|lib/Cryptol.cry|]
preludeContents = $(embedFileRelative "lib/Cryptol.cry")
preludeReferenceContents :: ByteString
preludeReferenceContents = B.pack [there|lib/Cryptol/Reference.cry|]
preludeReferenceContents = $(embedFileRelative "lib/Cryptol/Reference.cry")
floatContents :: ByteString
floatContents = B.pack [there|lib/Float.cry|]
floatContents = $(embedFileRelative "lib/Float.cry")
arrayContents :: ByteString
arrayContents = B.pack [there|lib/Array.cry|]
arrayContents = $(embedFileRelative "lib/Array.cry")
suiteBContents :: ByteString
suiteBContents = B.pack [there|lib/SuiteB.cry|]
suiteBContents = $(embedFileRelative "lib/SuiteB.cry")
primeECContents :: ByteString
primeECContents = B.pack [there|lib/PrimeEC.cry|]
primeECContents = $(embedFileRelative "lib/PrimeEC.cry")
cryptolTcContents :: String
cryptolTcContents = [there|lib/CryptolTC.z3|]
cryptolTcContents = B.unpack $(embedFileRelative "lib/CryptolTC.z3")