/usr/share/doc/why/examples/Makefile.common is in why-examples 2.34-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 | # Generated automatically from Makefile.common.in by configure.
WHYBIN=../../bin/why.opt
WHY=WHYLIB=../../lib $(WHYBIN) -split-user-conj
GWHY=WHYLIB=../../lib ../../bin/gwhy.opt -split-user-conj --lib-file arrays.why
CADUCEUS=WHYLIB=../../lib ../../bin/caduceus.opt
# WHYOPTIONS=--coq-v8
WHYOPTIONS=--coq-v8 --valid
DP=../../bin/why-dp.opt
dp: simplify cvcl
coq: $(VO:_valid.vo=_why.vo)
simplify: $(VO:_valid.vo=_why.sx)
$(DP) -timeout 10 $^ 2>/dev/null
yices: $(VO:_valid.vo=_why.smt)
$(DP) -smt-solver yices -timeout 10 $^ 2>/dev/null
z3: $(VO:_valid.vo=_why.z3.smt)
$(DP) -smt-solver z3 -timeout 10 $^ 2>/dev/null
z3smt: $(VO:_valid.vo=_why.smt)
$(DP) -smt-solver z3 -timeout 10 $^ 2>/dev/null
zenon: $(VO:_valid.vo=_why.znn)
$(DP) -timeout 10 $^ 2>/dev/null
cvcl: $(VO:_valid.vo=_why.cvc)
$(DP) -timeout 10 $^ 2>/dev/null
ergo: $(VO:_valid.vo=_why.why)
$(DP) -timeout 10 $^ 2>/dev/null
.PHONY: check
check: $(VO:_valid.vo=.check)
harvey: $(VO:_valid.vo=_why.rv)
$(DP) -timeout 10 $^ 2>/dev/null
%_valid.v %_why.v: %.mlw $(WHYBIN)
$(WHY) $(WHYOPTIONS) $<
%_valid.v %_why.v: %.c $(CADUCEUS)
$(CADUCEUS) $<
%_why.vo: %_why.v
coqc -I ../../lib/coq $(OPT) $<
%_valid.vo: %_valid.v %_why.vo
coqc -I ../../lib/coq $(OPT) $<
%.vo: %.v
coqc -I ../../lib/coq $(OPT) $<
%_why.pvs: %.mlw $(WHYBIN)
$(WHY) --pvs $<
%_why.sx: %.mlw $(WHYBIN)
$(WHY) --simplify $<
%_why.smt: %.mlw $(WHYBIN)
$(WHY) --smtlib --encoding sstrat $<
%_why.z3.smt: %.mlw $(WHYBIN)
$(WHY) --z3 --encoding sstrat $<
%_why.znn: %.mlw $(WHYBIN)
$(WHY) --zenon $<
%_why.cvc: %.mlw $(WHYBIN)
$(WHY) --cvcl $<
%_why.why: %.mlw $(WHYBIN)
$(WHY) --why $<
%_why.why: %.why $(WHYBIN)
$(WHY) --why $<
%.check: %.mlw $(WHYBIN)
$(WHYBIN) -tc $<
%.check: %.why $(WHYBIN)
$(WHYBIN) -tc $<
%_why.rv: %.mlw $(WHYBIN)
$(WHY) --harvey $<
%_why.miz: %.mlw $(WHYBIN)
$(WHY) --mizar $<
%_why.miz: %.c $(WHYBIN)
$(WHY) --mizar $<
%.ml: %.mlw
$(WHY) -ocaml $< > $@
ocamlc -c -i $@
%.wol: %.mlw
$(WHY) --wol $<
%.gui: %.mlw
$(GWHY) $<
%.gui: %.why
$(GWHY) $<
%.fastwp: %.mlw
$(GWHY) -fast-wp $<
clean::
rm -f *~ *.vo *.wol
rm -f *_valid.v
depend:: $(VO:.vo=.v)
coqdep -I ../../lib/coq *.v > .depend
include .depend
|