diff --git a/ml/build.cmd b/ml/build.cmd index 1624f460f..e3da5712b 100644 --- a/ml/build.cmd +++ b/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 \ No newline at end of file +ENDLOCAL diff --git a/ml/compile_mlapi.cmd b/ml/compile_mlapi.cmd index db80521dc..17776b6b8 100644 --- a/ml/compile_mlapi.cmd +++ b/ml/compile_mlapi.cmd @@ -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 diff --git a/ml/generate_mlapi.cmd b/ml/generate_mlapi.cmd index 8f64cb057..6a796a401 100644 --- a/ml/generate_mlapi.cmd +++ b/ml/generate_mlapi.cmd @@ -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. diff --git a/ml/test_mlapi.cmd b/ml/test_mlapi.cmd index 3d538a9df..64315e3f7 100644 --- a/ml/test_mlapi.cmd +++ b/ml/test_mlapi.cmd @@ -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.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 diff --git a/ml/update-ml-doc.cmd b/ml/update-ml-doc.cmd index 9d2409153..32c39109e 100644 --- a/ml/update-ml-doc.cmd +++ b/ml/update-ml-doc.cmd @@ -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|
val\(.*\)
|
val\1
|g;s|
type\(.*\)
|
type\1
|g;s|type\(.*\) = |
type\1 =
|g" Z3.html > Z3.new.html +sed "s|
val\(.*\)
|
val\1
|g;s|
type\(.*\)
|
type\1
|g;s|type\(.*\) = |
type\1 =
|g" Z3.html > Z3.new.html move >NUL Z3.new.html Z3.html -..\sed.exe "s|
val\(.*\)
|
val\1
|g" Test_mlapi.html > Test_mlapi.new.html +sed "s|
val\(.*\)
|
val\1
|g" Test_mlapi.html > Test_mlapi.new.html move >NUL Test_mlapi.new.html Test_mlapi.html -..\sed.exe "s|

Index of values

|

OCaml: Index

|" Index_values.html > Index_values.new.html +sed "s|

Index of values

|

OCaml: Index

|" 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