Skip to content

Commit

Permalink
use file-embed to make TH file embedding more robust
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Ptival committed Jan 23, 2024
1 parent 3b9f6c5 commit 6a02dda
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 13 deletions.
2 changes: 1 addition & 1 deletion cryptol.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -58,11 +58,11 @@ library
deepseq >= 1.3,
directory >= 1.2.2.0,
exceptions,
file-embed,
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,
Expand Down
22 changes: 10 additions & 12 deletions src/Cryptol/Prelude.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -23,28 +22,27 @@ module Cryptol.Prelude
, cryptolTcContents
) where

import Data.ByteString(ByteString)
import Data.ByteString (ByteString)
import Data.FileEmbed (embedFile, makeRelativeToProject)
import qualified Data.ByteString.Char8 as B
import Text.Heredoc (there)


preludeContents :: ByteString
preludeContents = B.pack [there|lib/Cryptol.cry|]
preludeContents = $(makeRelativeToProject "lib/Cryptol.cry" >>= embedFile)

preludeReferenceContents :: ByteString
preludeReferenceContents = B.pack [there|lib/Cryptol/Reference.cry|]
preludeReferenceContents = $(makeRelativeToProject "lib/Cryptol/Reference.cry" >>= embedFile)

floatContents :: ByteString
floatContents = B.pack [there|lib/Float.cry|]
floatContents = $(makeRelativeToProject "lib/Float.cry" >>= embedFile)

arrayContents :: ByteString
arrayContents = B.pack [there|lib/Array.cry|]
arrayContents = $(makeRelativeToProject "lib/Array.cry" >>= embedFile)

suiteBContents :: ByteString
suiteBContents = B.pack [there|lib/SuiteB.cry|]
suiteBContents = $(makeRelativeToProject "lib/SuiteB.cry" >>= embedFile)

primeECContents :: ByteString
primeECContents = B.pack [there|lib/PrimeEC.cry|]
primeECContents = $(makeRelativeToProject "lib/PrimeEC.cry" >>= embedFile)

cryptolTcContents :: String
cryptolTcContents = [there|lib/CryptolTC.z3|]
cryptolTcContents = B.unpack $(makeRelativeToProject "lib/CryptolTC.z3" >>= embedFile)

0 comments on commit 6a02dda

Please sign in to comment.