Compilation failed (line 28 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy"):
can't use native codegen on ARM64 target
usage: mlton [option ...] file.{c|mlb|o|sml} [file.{c|o|s|S} ...]
-align {8|4} object alignment
-as-opt <opt> pass option to assembler
-cc <cc> executable for C compiler
-cc-opt <opt> pass option to C compiler
-codegen {c|llvm} which code generator to use
-const '<name> <value>' set compile-time constant
-default-ann <ann> set annotation default for mlb files
-default-type '<ty><N>' set default type
-disable-ann <ann> disable annotation in mlb files
-export-header <file> write C header file for _export's
-ieee-fp {false|true} use strict IEEE floating-point
-inline <n> set inlining threshold
-keep {g|o} save intermediate files
-link-opt <opt> pass option to linker
-llvm-as <llvm-as> executable for llvm .ll -> .bc assembler
-llvm-as-opt <opt> pass option to llvm assembler
-llvm-llc <llc> executable for llvm .bc -> .o system compiler
-llvm-llc-opt <opt> pass option to llvm compiler
-llvm-opt <opt> executable for llvm .bc -> .bc optimizer
-llvm-opt-opt <opt> pass option to llvm optimizer
-mlb-path-map <file> additional MLB path map
-mlb-path-var '<name> <value>' additional MLB path var
-output <file> name of output file
-profile {no|alloc|count|time} produce executable suitable for profiling
-profile-branch {false|true} profile branches in addition to functions
-profile-stack {false|true} profile the stack
-profile-val {false|true} profile val bindings in addition to functions
-runtime <arg> pass arg to runtime via @MLton
-show-basis <file> write final basis environment
-show-def-use <file> write def-use information
-stop {f|g|o|tc} when to stop
-target {self} platform that executable will run on
-target-as-opt <target> <opt> target-dependent assembler option
-target-cc-opt <target> <opt> target-dependent C compiler option
-target-link-opt <target> <opt> target-dependent linker option
-verbose {0|1|2|3} how verbose to be
At command "compile_generated_files" (line 19 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy")