From 48c6c4aa8182ac79cb306854ea5b48d860723ce0 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 19 May 2020 16:24:23 +0100 Subject: [PATCH] Write Ints as 64 bit Since they might be... This is especially likely for module hashes, and if we don't get it right, the Racket runtime might fail to write the buffer. This makes the code buildable with the Racket back end. --- INSTALL.md | 7 +++++++ idris2.ipkg | 1 + src/Core/Binary.idr | 2 +- src/Utils/Binary.idr | 12 ++++++------ support/chez/support.ss | 8 +++++++- support/racket/support.rkt | 8 +++++++- 6 files changed, 29 insertions(+), 9 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index b540c1b6e..2cf380460 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -13,6 +13,13 @@ do this with `brew install coreutils`. If you have an existing Idris 2, go to step 1b. Otherwise, read on... +Make sure that: + +* `$PREFIX/bin` is in your `PATH` +* `$PREFIX/lib` is in your `LD_LIBRARY_PATH` (so that the system knows where + to look for library support code) + + 1a: Installing without an existing Idris 2 ------------------------------------------ diff --git a/idris2.ipkg b/idris2.ipkg index 5af5dbb57..10828c45b 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -143,6 +143,7 @@ modules = Yaffle.Main, Yaffle.REPL +-- opts = "--codegen racket" depends = contrib, network sourcedir = "src" diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 78e181750..c02bd6ace 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -28,7 +28,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 26 +ttcVersion = 27 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Utils/Binary.idr b/src/Utils/Binary.idr index 96392da07..5a1b63755 100644 --- a/src/Utils/Binary.idr +++ b/src/Utils/Binary.idr @@ -159,20 +159,20 @@ export TTC Int where toBuf b val = do chunk <- get Bin - if avail chunk >= 4 + if avail chunk >= 8 then do coreLift $ setInt (buf chunk) (loc chunk) val - put Bin (appended 4 chunk) - else do chunk' <- extendBinary 4 chunk + put Bin (appended 8 chunk) + else do chunk' <- extendBinary 8 chunk coreLift $ setInt (buf chunk') (loc chunk') val - put Bin (appended 4 chunk') + put Bin (appended 8 chunk') fromBuf b = do chunk <- get Bin - if toRead chunk >= 4 + if toRead chunk >= 8 then do val <- coreLift $ getInt (buf chunk) (loc chunk) - put Bin (incLoc 4 chunk) + put Bin (incLoc 8 chunk) pure val else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk)))) diff --git a/support/chez/support.ss b/support/chez/support.ss index 5e36f73de..2443dd0c2 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -97,9 +97,15 @@ (bytevector-u8-ref buf loc)) (define (blodwen-buffer-setint buf loc val) - (bytevector-s32-set! buf loc val (native-endianness))) + (bytevector-s64-set! buf loc val (native-endianness))) (define (blodwen-buffer-getint buf loc) + (bytevector-s64-ref buf loc (native-endianness))) + +(define (blodwen-buffer-setint32 buf loc val) + (bytevector-s32-set! buf loc val (native-endianness))) + +(define (blodwen-buffer-getint32 buf loc) (bytevector-s32-ref buf loc (native-endianness))) (define (blodwen-buffer-setdouble buf loc val) diff --git a/support/racket/support.rkt b/support/racket/support.rkt index 5a09e9309..487886366 100644 --- a/support/racket/support.rkt +++ b/support/racket/support.rkt @@ -85,9 +85,15 @@ (bytevector-u8-ref buf loc)) (define (blodwen-buffer-setint buf loc val) - (bytevector-s32-set! buf loc val (native-endianness))) + (bytevector-s64-set! buf loc val (native-endianness))) (define (blodwen-buffer-getint buf loc) + (bytevector-s64-ref buf loc (native-endianness))) + +(define (blodwen-buffer-setint32 buf loc val) + (bytevector-s32-set! buf loc val (native-endianness))) + +(define (blodwen-buffer-getint32 buf loc) (bytevector-s32-ref buf loc (native-endianness))) (define (blodwen-buffer-setdouble buf loc val)