Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-devel
Commits
be5e2dcd71e3
Commit
80c9aa17
authored
Feb 22, 2021
by
wenzelm
Browse files
adapted to Isabelle/f0db1e4c89bc;
parent
ec187af6fd41
Changes
3
Hide whitespace changes
Inline
Side-by-side
thys/CakeML/Tools/cakeml_compiler.ML
View file @
be5e2dcd
...
...
@@ -46,11 +46,12 @@ fun compile_ml_file mode source =
val
bash_cake
=
File
.
bash_path
(
compiler
()
)
val
bash_source
=
File
.
bash_path
source
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
bash_cake
^
" --sexp="
^
sexp
^
" < "
^
bash_source
)
val
res
=
Isabelle_System
.
bash_process
(
bash_cake
^
" --sexp="
^
sexp
^
" < "
^
bash_source
)
val
err
=
Process_Result
.
err
res
val
out
=
Process_Result
.
out
res
val
_
=
if
err
<>
""
then
warning
err
else
()
in
if
rc
<>
0
orelse
err
<>
""
then
if
not
(
Process_Result
.
ok
res
)
orelse
err
<>
""
then
error
"CakeML: ML compilation failed"
else
(
File
.
write
output
(
trim_line
out
);
output
)
...
...
@@ -71,12 +72,13 @@ fun compile_c_file source =
val
bash_cc
=
File
.
bash_path
(
Path
.
explode
(
getenv_strict
"ISABELLE_CC"
))
val
bash_source
=
File
.
bash_path
source
val
bash_output
=
File
.
bash_path
output
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
bash_cc
^
" -c -o "
^
bash_output
^
" "
^
bash_source
)
val
res
=
Isabelle_System
.
bash_process
(
bash_cc
^
" -c -o "
^
bash_output
^
" "
^
bash_source
)
val
err
=
Process_Result
.
err
res
val
out
=
Process_Result
.
out
res
val
_
=
if
err
<>
""
then
warning
err
else
()
val
_
=
writeln
out
in
if
rc
<>
0
orelse
err
<>
""
then
if
not
(
Process_Result
.
ok
res
)
orelse
err
<>
""
then
error
"CakeML: C compilation failed"
else
output
...
...
@@ -93,12 +95,13 @@ fun link sources =
val
bash_cc
=
File
.
bash_path
(
Path
.
explode
(
getenv_strict
"ISABELLE_CC"
))
val
bash_sources
=
Bash
.
strings
(
map
File
.
standard_path
sources
)
val
bash_output
=
File
.
bash_path
output
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
bash_cc
^
" -o "
^
bash_output
^
" "
^
bash_sources
)
val
res
=
Isabelle_System
.
bash_process
(
bash_cc
^
" -o "
^
bash_output
^
" "
^
bash_sources
)
val
err
=
Process_Result
.
err
res
val
out
=
Process_Result
.
out
res
val
_
=
if
err
<>
""
then
warning
err
else
()
val
_
=
writeln
out
in
if
rc
<>
0
orelse
err
<>
""
then
if
not
(
Process_Result
.
ok
res
)
orelse
err
<>
""
then
error
"CakeML: linking failed"
else
output
...
...
@@ -109,10 +112,12 @@ fun eval mode source =
val
cake
=
compile_ml
mode
source
val
ffi
=
compile_ffi
()
val
bin
=
link
[
cake
,
ffi
]
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
File
.
bash_path
bin
)
val
res
=
Isabelle_System
.
bash_process
(
File
.
bash_path
bin
)
val
err
=
Process_Result
.
err
res
val
out
=
Process_Result
.
out
res
val
_
=
if
err
<>
""
then
warning
err
else
()
in
if
rc
<>
0
orelse
err
<>
""
then
if
not
(
Process_Result
.
ok
res
)
orelse
err
<>
""
then
error
"CakeML: evaluation failed"
else
trim_line
out
...
...
thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy
View file @
be5e2dcd
...
...
@@ -643,10 +643,11 @@ structure Export_code_env = struct
end
fun compile l cmd =
let val (l, rc) = fold (fn cmd => (fn (l, 0) =>
let val {out, err, rc, ...} = Isabelle_System.bash_process cmd in
((out, err) :: l, rc) end
| x => x)) l ([], 0)
let val (l, rc) = fold (fn cmd =>
(fn (l, 0) =>
let val res = Isabelle_System.bash_process cmd in
((Process_Result.out res, Process_Result.err res) :: l, Process_Result.rc res) end
| x => x)) l ([], 0)
val l = rev l in
if rc = 0 then
(l, Isabelle_System.bash_output cmd)
...
...
thys/Randomised_Social_Choice/Automation/QSOpt_Exact.thy
View file @
be5e2dcd
...
...
@@ -358,11 +358,11 @@ fun solve_program prog =
val esolver_path = getenv "QSOPT_EXACT_PATH"
val esolver = if esolver_path = "" then "esolver" else esolver_path
val command = wrap esolver ^ " -O " ^ wrap resultname ^ " " ^ wrap lpname
val
{err, rc, ...}
= Isabelle_System.bash_process command
val
res
= Isabelle_System.bash_process command
in
if
rc <> 0
then
if
not (Process_Result.ok res)
then
raise Fail ("QSopt_exact returned with an error (return code " ^
Int.toString
rc ^ "):\n" ^ err
)
Int.toString
(Process_Result.rc res) ^ "):\n" ^ Process_Result.err res
)
else
let
val result = read_result_file resultname
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment