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
fedf84a4c625
Commit
e28a8dcf
authored
Feb 20, 2021
by
wenzelm
Browse files
adapted to Isabelle/440546ea20e6;
parent
4b87cdc4baaf
Changes
4
Hide whitespace changes
Inline
Side-by-side
thys/CakeML/Tools/cakeml_compiler.ML
View file @
fedf84a4
...
...
@@ -46,7 +46,8 @@ fun compile_ml_file mode source =
val
bash_cake
=
File
.
bash_path
(
compiler
()
)
val
bash_source
=
File
.
bash_path
source
val
{
out
,
err
,
rc
,
...
}
=
Bash
.
process
(
bash_cake
^
" --sexp="
^
sexp
^
" < "
^
bash_source
)
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
bash_cake
^
" --sexp="
^
sexp
^
" < "
^
bash_source
)
val
_
=
if
err
<>
""
then
warning
err
else
()
in
if
rc
<>
0
orelse
err
<>
""
then
...
...
@@ -70,7 +71,8 @@ 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
,
...
}
=
Bash
.
process
(
bash_cc
^
" -c -o "
^
bash_output
^
" "
^
bash_source
)
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
bash_cc
^
" -c -o "
^
bash_output
^
" "
^
bash_source
)
val
_
=
if
err
<>
""
then
warning
err
else
()
val
_
=
writeln
out
in
...
...
@@ -91,7 +93,8 @@ 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
,
...
}
=
Bash
.
process
(
bash_cc
^
" -o "
^
bash_output
^
" "
^
bash_sources
)
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_process
(
bash_cc
^
" -o "
^
bash_output
^
" "
^
bash_sources
)
val
_
=
if
err
<>
""
then
warning
err
else
()
val
_
=
writeln
out
in
...
...
@@ -106,7 +109,7 @@ fun eval mode source =
val
cake
=
compile_ml
mode
source
val
ffi
=
compile_ffi
()
val
bin
=
link
[
cake
,
ffi
]
val
{
out
,
err
,
rc
,
...
}
=
Bash
.
process
(
File
.
bash_path
bin
)
val
{
out
,
err
,
rc
,
...
}
=
Isabelle_System
.
bash_
process
(
File
.
bash_path
bin
)
val
_
=
if
err
<>
""
then
warning
err
else
()
in
if
rc
<>
0
orelse
err
<>
""
then
...
...
thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy
View file @
fedf84a4
...
...
@@ -644,7 +644,7 @@ end
fun compile l cmd =
let val (l, rc) = fold (fn cmd => (fn (l, 0) =>
let val {out, err, rc, ...} =
Bash.
process cmd in
let val {out, err, rc, ...} =
Isabelle_System.bash_
process cmd in
((out, err) :: l, rc) end
| x => x)) l ([], 0)
val l = rev l in
...
...
thys/Network_Security_Policy_Verification/Lib/ML_GraphViz.thy
View file @
fedf84a4
...
...
@@ -101,8 +101,8 @@ local
(Isabelle_System.bash o cat_lines)
["set -e",
"cd " ^ File.bash_path (Path.dir graph_file),
"\"$ISABELLE_DOT\" -o " ^ Bash
_Syntax
.string (File.platform_path pdf_file) ^
" -Tpdf " ^ Bash
_Syntax
.string (File.platform_path graph_file),
"\"$ISABELLE_DOT\" -o " ^ Bash.string (File.platform_path pdf_file) ^
" -Tpdf " ^ Bash.string (File.platform_path graph_file),
"\"$PDF_VIEWER\" " ^ File.bash_path pdf_file ^ " &"];
in () end);
...
...
thys/Randomised_Social_Choice/Automation/QSOpt_Exact.thy
View file @
fedf84a4
...
...
@@ -358,7 +358,7 @@ 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
= err, rc = rc, ...} = B
ash
.
process command
val {err
, rc, ...} = Isabelle_System.b
ash
_
process command
in
if rc <> 0 then
raise Fail ("QSopt_exact returned with an error (return code " ^
...
...
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