proper build_call for interpreted ARM platform;
authorwenzelm
Sun, 01 Nov 2020 15:31:41 +0100
changeset 72535 7cb68b5b103d
parent 72534 e0c6522d5d43
child 72536 589645894305
child 72537 18eed4f718e0
proper build_call for interpreted ARM platform;
src/Pure/General/sha1.ML
src/Pure/ML/ml_system.ML
--- a/src/Pure/General/sha1.ML	Sun Nov 01 14:30:09 2020 +0100
+++ b/src/Pure/General/sha1.ML	Sun Nov 01 15:31:41 2020 +0100
@@ -148,11 +148,14 @@
 val library_path =
   Path.explode ("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so"));
 
-val library_call =
+fun build_call () =
   Foreign.buildCall3
     (Foreign.getSymbol (Foreign.loadLibrary (File.platform_path library_path)) "sha1_buffer",
       (Foreign.cByteArray, Foreign.cUlong, Foreign.cPointer), Foreign.cPointer);
 
+val library_call =
+  if ML_System.platform_is_arm then fn args => build_call () args else build_call ();
+
 fun with_memory n =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn f =>
     let
--- a/src/Pure/ML/ml_system.ML	Sun Nov 01 14:30:09 2020 +0100
+++ b/src/Pure/ML/ml_system.ML	Sun Nov 01 15:31:41 2020 +0100
@@ -10,6 +10,7 @@
   val platform: string
   val platform_is_windows: bool
   val platform_is_64: bool
+  val platform_is_arm: bool
   val platform_path: string -> string
   val standard_path: string -> string
 end;
@@ -21,6 +22,7 @@
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_windows = String.isSuffix "windows" platform;
 val platform_is_64 = String.isPrefix "x86_64-" platform;
+val platform_is_arm = String.isPrefix "arm64-" platform;
 
 val platform_path =
   if platform_is_windows then