Xiaokun Luan (Oct 17 2023 at 05:49): Xiaokun Luan (Oct 17 2023 at 05:49):Hi guys, I got the following errors when I was trying to build HOL sessions, it seems that MLton is not working as expected, any idea how to fix this?
*** Compilation with MLton failed:
5 *** "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-luanxiaokun/ ↪process6572602058989807230/Code_Test13776872/test.mlb
4 ***
3 *** At command "value" (line 11 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
2 *** Compilation with MLton failed:
1 *** "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-luanxiaokun/ ↪process6572602058989807230/Code_Test13776870/test.mlb
7 *** 1 *** At command "test_code" (line 13 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
2 *** Compilation with MLton failed:
3 *** "$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS -default-type intinf /tmp/isabelle-luanxiaokun/ ↪process6572602058989807230/Code_Test13776874/test.mlb
4 ***
5 *** At command "test_code" (line 9 of "~~/src/HOL/Codegenerator_Test/Code_Test_MLton.thy")
By the way, I am using Isabelle2022, I checked $ISABELLE_MLTON, it seems fine.
Zenan Li (Nov 01 2023 at 06:27):I encountered the same issue, has it been resolved yet?
Xiaokun Luan (Nov 02 2023 at 03:22):Zenan Li said:
I encountered the same issue, has it been resolved yet?
No, not yet
Last updated: Apr 27 2024 at 20:14 UTC