Skip to content

Commit e3f3a3b

Browse files
committed
still trying to fix the vampire build in github actions
1 parent 49cdace commit e3f3a3b

File tree

1 file changed

+58
-10
lines changed

1 file changed

+58
-10
lines changed

patchVampireInteractive.sh

Lines changed: 58 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -195,11 +195,7 @@ run_patch "Avoid random_device failure in WASM" '--- a/Lib/Random.hpp
195195
+ inline static unsigned systemSeed()
196196
+ {
197197
+#ifdef __EMSCRIPTEN__
198-
+ try {
199-
+ return std::random_device()();
200-
+ } catch (...) {
201-
+ return static_cast<unsigned>(std::time(nullptr));
202-
+ }
198+
+ return static_cast<unsigned>(std::time(nullptr));
203199
+#else
204200
+ return std::random_device()();
205201
+#endif
@@ -235,6 +231,32 @@ run_patch "Use Random::systemSeed in PortfolioMode" '--- a/CASC/PortfolioMode.cp
235231
+ opt.setRandomSeed(Random::systemSeed());
236232
'
237233

234+
run_patch "Disable portfolio mode on WASM" '--- a/CASC/PortfolioMode.cpp
235+
+++ b/CASC/PortfolioMode.cpp
236+
@@
237+
bool PortfolioMode::perform(Problem* problem)
238+
{
239+
+#ifdef __EMSCRIPTEN__
240+
+ std::cerr << "% Portfolio mode is not supported in WebAssembly builds." << std::endl;
241+
+ return false;
242+
+#endif
243+
PortfolioMode pm(problem);
244+
'
245+
246+
run_patch "Force non-portfolio mode on WASM" '--- a/vampire.cpp
247+
+++ b/vampire.cpp
248+
@@
249+
Shell::CommandLine cl(argc, argv);
250+
cl.interpret(opts);
251+
+#ifdef __EMSCRIPTEN__
252+
+ if (opts.mode() == Options::Mode::CASC ||
253+
+ opts.mode() == Options::Mode::SMTCOMP ||
254+
+ opts.mode() == Options::Mode::PORTFOLIO) {
255+
+ std::cerr << "% WASM build: forcing --mode vampire (portfolio disabled)" << std::endl;
256+
+ opts.setMode(Options::Mode::VAMPIRE);
257+
+ }
258+
+#endif
259+
238260
run_patch "Relax TermOrderingDiagram asserts for Emscripten" '--- a/Kernel/TermOrderingDiagram.hpp
239261
+++ b/Kernel/TermOrderingDiagram.hpp
240262
@@
@@ -282,11 +304,7 @@ insert = (
282304
" inline static unsigned systemSeed()\n"
283305
" {\n"
284306
"#ifdef __EMSCRIPTEN__\n"
285-
" try {\n"
286-
" return std::random_device()();\n"
287-
" } catch (...) {\n"
288-
" return static_cast<unsigned>(std::time(nullptr));\n"
289-
" }\n"
307+
" return static_cast<unsigned>(std::time(nullptr));\n"
290308
"#else\n"
291309
" return std::random_device()();\n"
292310
"#endif\n"
@@ -333,12 +351,42 @@ text = path.read_text()
333351
if "Lib/Random.hpp" not in text:
334352
text = text.replace('#include "Lib/Timer.hpp"\\n', '#include "Lib/Timer.hpp"\\n#include "Lib/Random.hpp"\\n', 1)
335353
text = text.replace("opt.setRandomSeed(std::random_device()());", "opt.setRandomSeed(Random::systemSeed());")
354+
if "Portfolio mode is not supported in WebAssembly" not in text:
355+
marker = "bool PortfolioMode::perform(Problem* problem)\\n{\\n"
356+
if marker in text:
357+
text = text.replace(marker, marker + "#ifdef __EMSCRIPTEN__\\n std::cerr << \"% Portfolio mode is not supported in WebAssembly builds.\" << std::endl;\\n return false;\\n#endif\\n", 1)
336358
path.write_text(text)
337359
PY
338360
echo "Applied: Use Random::systemSeed in PortfolioMode (fallback)"
339361
fi
340362
fi
341363

364+
# Fallback: force mode vampire on WASM in vampire.cpp
365+
VAMP_PATH="$ROOT_DIR/vampire.cpp"
366+
if [[ -f "$VAMP_PATH" ]]; then
367+
if ! grep -q "WASM build: forcing --mode vampire" "$VAMP_PATH"; then
368+
python - <<PY
369+
from pathlib import Path
370+
path = Path(r"$VAMP_PATH")
371+
text = path.read_text()
372+
marker = "cl.interpret(opts);\\n"
373+
inject = ("cl.interpret(opts);\\n"
374+
"#ifdef __EMSCRIPTEN__\\n"
375+
" if (opts.mode() == Options::Mode::CASC ||\\n"
376+
" opts.mode() == Options::Mode::SMTCOMP ||\\n"
377+
" opts.mode() == Options::Mode::PORTFOLIO) {\\n"
378+
" std::cerr << \"% WASM build: forcing --mode vampire (portfolio disabled)\" << std::endl;\\n"
379+
" opts.setMode(Options::Mode::VAMPIRE);\\n"
380+
" }\\n"
381+
"#endif\\n")
382+
if marker in text:
383+
text = text.replace(marker, inject, 1)
384+
path.write_text(text)
385+
PY
386+
echo "Applied: Force non-portfolio mode on WASM (fallback)"
387+
fi
388+
fi
389+
342390
run_patch "List WebInteractive.cpp in sources" '--- a/cmake/sources.cmake
343391
+++ b/cmake/sources.cmake
344392
@@

0 commit comments

Comments
 (0)