mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
updated ml build scripts to assume required tools are already set up, and added comments specifying which tools are required
This commit is contained in:
Josh Berdine
parent
452ea65189
commit
aec36146ab
5 changed files with 31 additions and 22 deletions
12
ml/build.cmd
12
ml/build.cmd
|
|
@ -2,7 +2,11 @@
|
|||
SETLOCAL
|
||||
|
||||
REM Script to generate, compile, test, and document the Z3 OCaml API
|
||||
REM
|
||||
REM Assumes that environment variables are set to provide access to the C and OCaml compilers, including flexdll and camlidl, as well as the following commands: diff, dos2unix, grep, sed, unix2dos
|
||||
REM
|
||||
REM usage: build.cmd [32|64] [-D UNSAFE_ERRORS] [-D LEAK_CONTEXTS]
|
||||
REM
|
||||
REM Invoke with "-D UNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead.
|
||||
REM Invoke with "-D LEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead.
|
||||
|
||||
|
|
@ -22,12 +26,6 @@ if %BITS% == 32 (
|
|||
set Z3DBG= ..\x64\Debug
|
||||
)
|
||||
|
||||
echo { Setting up environment
|
||||
call "C:\Program Files (x86)\Microsoft Visual Studio 10.0\VC\vcvarsall.bat" %ARCH%
|
||||
call ..\tools\ocaml\win%BITS%\setup.cmd
|
||||
set PATH=..\tools;..\mlV3;%PATH%
|
||||
echo }
|
||||
|
||||
echo { Cleaning
|
||||
call .\clean.cmd
|
||||
echo }
|
||||
|
|
@ -52,4 +50,4 @@ call .\update-ml-doc.cmd ..\doc
|
|||
if errorlevel 1 goto :EOF
|
||||
echo }
|
||||
|
||||
ENDLOCAL
|
||||
ENDLOCAL
|
||||
|
|
|
|||
|
|
@ -2,7 +2,10 @@
|
|||
SETLOCAL
|
||||
|
||||
REM Script to compile the Z3 OCaml API
|
||||
REM
|
||||
REM Compiles byte and debug native code versions with debug info, optimized native code versions without
|
||||
REM
|
||||
REM Assumes that environment variables are set to provide access to the C and OCaml compilers
|
||||
|
||||
REM directory containing z3_api.h
|
||||
set Z3SRC=%1
|
||||
|
|
|
|||
|
|
@ -1,6 +1,9 @@
|
|||
@echo off
|
||||
|
||||
REM Script to generate the Z3 OCaml API
|
||||
REM
|
||||
REM Assumes that environment variables are set to provide access to the following commands: camlidl, dos2unix, grep, sed, unix2dos
|
||||
REM
|
||||
REM Invoke with "-D UNSAFE_ERRORS" to build version that does not support recoverable errors, but avoids some error-checking overhead.
|
||||
REM Invoke with "-D LEAK_CONTEXTS" to build version that leaks Z3_context objects, but avoids some garbage-collection overhead.
|
||||
|
||||
|
|
|
|||
|
|
@ -2,6 +2,8 @@
|
|||
SETLOCAL
|
||||
|
||||
REM Script to test the Z3 OCaml API
|
||||
REM
|
||||
REM Assumes that environment variables are set to provide access to the C and OCaml compilers, as well as the following commands: diff, dos2unix, sed
|
||||
|
||||
REM directory containing z3_api.h
|
||||
set Z3SRC=%1
|
||||
|
|
@ -46,13 +48,14 @@ sed <queen.orig.err >queen.err "s/ \[.*\]/ [...]/g"
|
|||
del test_capi.orig.err test_mlapi.orig.err test_mlapiV3.orig.err queen.orig.err
|
||||
|
||||
REM Compare with regressions
|
||||
diff test_capi.regress.out test_capi.out >NUL || echo Regression failed, see: windiff test_capi.regress.out test_capi.out
|
||||
diff test_mlapi.regress.out test_mlapi.out >NUL || echo Regression failed, see: windiff test_mlapi.regress.out test_mlapi.out
|
||||
diff test_mlapiV3.regress.out test_mlapiV3.out >NUL || echo Regression failed, see: windiff test_mlapiV3.regress.out test_mlapiV3.out
|
||||
diff test_capi.regress.err test_capi.err >NUL || echo Regression failed, see: windiff test_capi.regress.err test_capi.err
|
||||
diff test_mlapi.regress.err test_mlapi.err >NUL || echo Regression failed, see: windiff test_mlapi.regress.err test_mlapi.err
|
||||
diff test_mlapiV3.regress.err test_mlapiV3.err >NUL || echo Regression failed, see: windiff test_mlapiV3.regress.err test_mlapiV3.err
|
||||
diff queen.regress.out queen.out >NUL || echo Regression failed, see: windiff queen.regress.out queen.out
|
||||
diff queen.regress.err queen.err >NUL || echo Regression failed, see: windiff queen.regress.err queen.err
|
||||
dos2unix *.out *.err 2>NUL
|
||||
diff test_capi.regress.out test_capi.out >NUL || echo Regression failed, see: diff test_capi.regress.out test_capi.out
|
||||
diff test_mlapi.regress.out test_mlapi.out >NUL || echo Regression failed, see: diff test_mlapi.regress.out test_mlapi.out
|
||||
diff test_mlapiV3.regress.out test_mlapiV3.out >NUL || echo Regression failed, see: diff test_mlapiV3.regress.out test_mlapiV3.out
|
||||
diff test_capi.regress.err test_capi.err >NUL || echo Regression failed, see: diff test_capi.regress.err test_capi.err
|
||||
diff test_mlapi.regress.err test_mlapi.err >NUL || echo Regression failed, see: diff test_mlapi.regress.err test_mlapi.err
|
||||
diff test_mlapiV3.regress.err test_mlapiV3.err >NUL || echo Regression failed, see: diff test_mlapiV3.regress.err test_mlapiV3.err
|
||||
diff queen.regress.out queen.out >NUL || echo Regression failed, see: diff queen.regress.out queen.out
|
||||
diff queen.regress.err queen.err >NUL || echo Regression failed, see: diff queen.regress.err queen.err
|
||||
|
||||
ENDLOCAL
|
||||
|
|
|
|||
|
|
@ -1,7 +1,9 @@
|
|||
@echo off
|
||||
SETLOCAL
|
||||
|
||||
call ..\tools\ocaml\win32\setup.cmd
|
||||
REM Script to generate Z3 OCaml API documentation
|
||||
REM
|
||||
REM Assumes that environment variables are set to provide access to the OCaml compilers, as well as the following commands: sed
|
||||
|
||||
rd 2>NUL /s /q doc
|
||||
md doc
|
||||
|
|
@ -9,26 +11,26 @@ cd doc
|
|||
set MLDIR=..
|
||||
set DOCDIR=..\%1
|
||||
|
||||
ocamldoc.opt.exe -hide Z3,Z3.V3,Test_mlapi -html -css-style z3_ml.css -I %MLDIR% %MLDIR%\test_mlapi.ml %MLDIR%\z3.mli
|
||||
ocamldoc.opt -hide Z3,Z3.V3,Test_mlapi -html -css-style z3_ml.css -I %MLDIR% %MLDIR%\test_mlapi.ml %MLDIR%\z3.mli
|
||||
|
||||
..\sed.exe "s|<pre><span class=\"keyword\">val\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">val\1</div>|g;s|<pre><span class=\"keyword\">type\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">type\1</div>|g;s|<code><span class=\"keyword\">type\(.*\) = </code>|<div class=\"function\"><span class=\"keyword\">type\1 = </div>|g" Z3.html > Z3.new.html
|
||||
sed "s|<pre><span class=\"keyword\">val\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">val\1</div>|g;s|<pre><span class=\"keyword\">type\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">type\1</div>|g;s|<code><span class=\"keyword\">type\(.*\) = </code>|<div class=\"function\"><span class=\"keyword\">type\1 = </div>|g" Z3.html > Z3.new.html
|
||||
move >NUL Z3.new.html Z3.html
|
||||
|
||||
..\sed.exe "s|<pre><span class=\"keyword\">val\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">val\1</div>|g" Test_mlapi.html > Test_mlapi.new.html
|
||||
sed "s|<pre><span class=\"keyword\">val\(.*\)</pre>|<div class=\"function\"><span class=\"keyword\">val\1</div>|g" Test_mlapi.html > Test_mlapi.new.html
|
||||
move >NUL Test_mlapi.new.html Test_mlapi.html
|
||||
|
||||
..\sed.exe "s|<h1>Index of values</h1>|<h1>OCaml: Index</h1>|" Index_values.html > Index_values.new.html
|
||||
sed "s|<h1>Index of values</h1>|<h1>OCaml: Index</h1>|" Index_values.html > Index_values.new.html
|
||||
move >NUL Index_values.new.html Index_values.html
|
||||
|
||||
copy >NUL %DOCDIR%\tabs.css
|
||||
copy >NUL %DOCDIR%\z3.png
|
||||
copy >NUL %DOCDIR%\z3_ml.css
|
||||
|
||||
..\sed.exe "1,23d" Test_mlapi.html | ..\sed.exe "$d" > Test_mlapi.new.html
|
||||
sed "1,23d" Test_mlapi.html | sed "$d" > Test_mlapi.new.html
|
||||
|
||||
type 2>NUL %DOCDIR%\test_mlapi_header.html Test_mlapi.new.html %DOCDIR%\mldoc_footer.html >Test_mlapi.html
|
||||
|
||||
..\sed.exe "1,37d" Z3.html > Z3.new.html
|
||||
sed "1,37d" Z3.html > Z3.new.html
|
||||
|
||||
type 2>NUL %DOCDIR%\z3_mlapi_header.html Z3.new.html >Z3.html
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue