Skip to content

Commit

Permalink
[Holmake] Revise HOL_LNSIGOBJ to not "link" selftest.{uo,ui}
Browse files Browse the repository at this point in the history
When running in parallel, different threads racing to link selftest
files in the sigobj directory can cause failures. Given that these
files play no useful role, we can avoid the races by simply not
moving/linking files called selftest.{uo,ui}.
  • Loading branch information
mn200 committed Aug 11, 2023
1 parent e059b8f commit 33ec7d9
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions tools/Holmake/Holmake_types.sml
Original file line number Diff line number Diff line change
Expand Up @@ -383,11 +383,14 @@ val base_environment0 = let
"$(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml)))")]),
("HOLDIR", [LIT HOLDIR]),
("HOL_LNSIGOBJ",
[LIT "for i in *.uo *.ui ; do ln -fs `pwd`/",
[LIT "for i in `pwd`/",
VREF "HOLOBJDIR", LIT "/*.uo `pwd`/",
VREF "HOLOBJDIR",
LIT "/$i ",
LIT "/*.ui ; do b=`basename $i` ; \
\if [ \"$b\" = \"selftest.uo\" -o \"$b\" = \"selftest.ui\" ] ; \
\then : ; else ln -fs $i ",
VREF "SIGOBJ",
LIT " ; done && for i in *.sig ; do ln -fs `pwd`/$i ",
LIT " ; fi ; done && for i in *.sig ; do ln -fs `pwd`/$i ",
VREF "SIGOBJ",
LIT " ; echo `pwd`/`basename $i .sig` >> ",
VREF "SIGOBJ",
Expand Down

0 comments on commit 33ec7d9

Please sign in to comment.