Skip to content

Commit af241e4

Browse files
mserimseri
authored
Merge pull request #24070 from maroneze/master
why3: ensure configure works with Cygwin
2 parents 3e875d8 + ad8cf93 commit af241e4

File tree

2 files changed

+185
-0
lines changed

2 files changed

+185
-0
lines changed

‎packages/why3/why3.1.6.0/files/cygwin.patch‎

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
diff --git a/configure.in b/configure.in
2+
index 0002665c0..9cb7151eb 100644
3+
--- a/configure.in
4+
+++ b/configure.in
5+
@@ -320,7 +320,7 @@ if test "$enable_ocamlfind" != no; then
6+
if test "$OCAMLFIND" = no; then
7+
reason_ocamlfind=" (not found)"
8+
else
9+
- OCAMLFINDLIB=$(ocamlfind printconf stdlib)
10+
+ OCAMLFINDLIB=$(ocamlfind printconf stdlib | tr -d '\r')
11+
if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then
12+
found_ocamlfind=no
13+
reason_ocamlfind=" (incompatible with OCaml)"
14+
@@ -341,7 +341,7 @@ fi
15+
16+
if test "$enable_ocamlfind" != no; then
17+
#if ocamlfind is used it gives the install path for ocaml library
18+
- OCAMLINSTALLLIB=$($OCAMLFIND printconf destdir)
19+
+ OCAMLINSTALLLIB=$($OCAMLFIND printconf destdir | tr -d '\r')
20+
enable_ocamlfind=yes
21+
else
22+
OCAMLINSTALLLIB=$OCAMLLIB
23+
@@ -356,7 +356,7 @@ else
24+
fi
25+
WHY3LIB=why3
26+
AC_MSG_CHECKING([for Why3 using ocamlfind])
27+
- DIR=$($OCAMLFIND query why3 2> /dev/null)
28+
+ DIR=$($OCAMLFIND query why3 | tr -d '\r' 2> /dev/null)
29+
if test -n "$DIR"; then
30+
AC_MSG_RESULT([yes])
31+
WHY3INCLUDE="-I $DIR"
32+
@@ -375,7 +375,7 @@ fi
33+
# ppx
34+
if test "$enable_ocamlfind" = yes; then
35+
AC_MSG_CHECKING([for compiler-libs using ocamlfind])
36+
- COMPILERLIBS=$($OCAMLFIND query compiler-libs 2> /dev/null)
37+
+ COMPILERLIBS=$($OCAMLFIND query compiler-libs | tr -d '\r' 2> /dev/null)
38+
if test -n "$COMPILERLIBS"; then
39+
AC_MSG_RESULT([yes])
40+
enable_ppx=yes
41+
@@ -425,7 +425,7 @@ fi
42+
found_num=no
43+
if test "$enable_ocamlfind" = yes; then
44+
AC_MSG_CHECKING([for num using ocamlfind])
45+
- DIR=$($OCAMLFIND query num 2> /dev/null)
46+
+ DIR=$($OCAMLFIND query num | tr -d '\r' 2> /dev/null)
47+
if test -z "$DIR"; then
48+
AC_MSG_RESULT([no])
49+
AC_MSG_ERROR([cannot find library Num using ocamlfind.])
50+
@@ -456,7 +456,7 @@ else
51+
found_zarith=yes
52+
if test "$enable_ocamlfind" = yes; then
53+
AC_MSG_CHECKING([for zarith using ocamlfind])
54+
- DIR=$($OCAMLFIND query zarith 2> /dev/null)
55+
+ DIR=$($OCAMLFIND query zarith | tr -d '\r' 2> /dev/null)
56+
if test -n "$DIR"; then
57+
AC_MSG_RESULT([yes])
58+
BIGINTINCLUDE="-I $DIR"
59+
@@ -496,7 +496,7 @@ fi
60+
if test "$enable_bddinfer" = yes; then
61+
if test "$enable_ocamlfind" = yes; then
62+
# gmp is a dependency of apron
63+
- INFERINCLUDE=$($OCAMLFIND query -separator ' ' -i-format apron 2> /dev/null)
64+
+ INFERINCLUDE=$($OCAMLFIND query -separator ' ' -i-format apron | tr -d '\r' 2> /dev/null)
65+
fi
66+
if test -n "$INFERINCLUDE"; then
67+
echo "ocamlfind found apron in $INFERINCLUDE"
68+
@@ -515,14 +515,14 @@ fi
69+
if test "$enable_infer" = yes; then
70+
if test "$enable_ocamlfind" = yes; then
71+
# gmp is a dependency of apron
72+
- INFERINCLUDE=$($OCAMLFIND query apron camllib 2> /dev/null)
73+
+ INFERINCLUDE=$($OCAMLFIND query apron camllib | tr -d '\r' 2> /dev/null)
74+
fi
75+
if test -n "$INFERINCLUDE"; then
76+
echo "ocamlfind found apron, camllib in $INFERINCLUDE"
77+
- INFERINCLUDE=$($OCAMLFIND query fixpoint 2> /dev/null)
78+
+ INFERINCLUDE=$($OCAMLFIND query fixpoint | tr -d '\r' 2> /dev/null)
79+
if test -n "$INFERINCLUDE"; then
80+
echo "ocamlfind found fixpoint in $INFERINCLUDE"
81+
- INFERINCLUDE="$($OCAMLFIND query -separator ' ' -i-format apron fixpoint camllib gmp 2> /dev/null)"
82+
+ INFERINCLUDE="$($OCAMLFIND query -separator ' ' -i-format apron fixpoint camllib gmp | tr -d '\r' 2> /dev/null)"
83+
INFERLIB="apron fixpoint"
84+
INFERPKG="apron fixpoint apron.boxMPQ apron.octMPQ apron.polkaMPQ"
85+
else
86+
@@ -547,7 +547,7 @@ else
87+
found_zip=yes
88+
if test "$enable_ocamlfind" = yes; then
89+
AC_MSG_CHECKING([for camlzip using ocamlfind])
90+
- DIR=$($OCAMLFIND query zip 2> /dev/null)
91+
+ DIR=$($OCAMLFIND query zip | tr -d '\r' 2> /dev/null)
92+
if test -n "$DIR"; then
93+
AC_MSG_RESULT([yes])
94+
ZIPINCLUDE="-I $DIR"
95+
@@ -586,7 +586,7 @@ found_menhirlib=yes
96+
DIR=
97+
if test "$enable_ocamlfind" = yes; then
98+
AC_MSG_CHECKING([for menhirLib using ocamlfind])
99+
- DIR=$($OCAMLFIND query menhirLib 2> /dev/null)
100+
+ DIR=$($OCAMLFIND query menhirLib | tr -d '\r' 2> /dev/null)
101+
if test -n "$DIR"; then
102+
AC_MSG_RESULT([yes])
103+
MENHIRINCLUDE="-I $DIR"
104+
@@ -618,7 +618,7 @@ else
105+
DIR=
106+
if test "$enable_ocamlfind" = yes; then
107+
AC_MSG_CHECKING([for re using ocamlfind])
108+
- DIR=$($OCAMLFIND query re 2> /dev/null)
109+
+ DIR=$($OCAMLFIND query re | tr -d '\r' 2> /dev/null)
110+
if test -n "$DIR"; then
111+
AC_MSG_RESULT([yes])
112+
REINCLUDE="-I $DIR"
113+
@@ -667,7 +667,7 @@ fi
114+
found_lablgtk=no
115+
if test "$enable_ide" != no; then
116+
AC_MSG_CHECKING([for lablgtk3 using ocamlfind])
117+
- DIR=$($OCAMLFIND query lablgtk3 2> /dev/null)
118+
+ DIR=$($OCAMLFIND query lablgtk3 | tr -d '\r' 2> /dev/null)
119+
if test -n "$DIR"; then
120+
AC_MSG_RESULT([yes])
121+
found_lablgtk=yes
122+
@@ -687,7 +687,7 @@ found_lablgtksourceview=no
123+
if test "$found_lablgtk" = yes; then
124+
for p in $PKGS_SOURCEVIEW; do
125+
AC_MSG_CHECKING([for $p using ocamlfind])
126+
- DIR=$($OCAMLFIND query $p 2> /dev/null)
127+
+ DIR=$($OCAMLFIND query $p | tr -d '\r' 2> /dev/null)
128+
if test -n "$DIR"; then
129+
AC_MSG_RESULT([yes])
130+
AC_CHECK_FILE($DIR/gSourceView$GTKVERSION.cmi,,p=)
131+
@@ -732,7 +732,7 @@ if test "$enable_hypothesis_selection" != no -o "$enable_stackify" != no; then
132+
DIR=
133+
if test "$enable_ocamlfind" = yes; then
134+
AC_MSG_CHECKING([for ocamlgraph using ocamlfind])
135+
- DIR=$($OCAMLFIND query ocamlgraph 2> /dev/null)
136+
+ DIR=$($OCAMLFIND query ocamlgraph | tr -d '\r' 2> /dev/null)
137+
if test -n "$DIR"; then
138+
AC_MSG_RESULT([yes])
139+
OCAMLGRAPHLIB="$DIR"
140+
@@ -802,14 +802,14 @@ elif test "$enable_js_of_ocaml" = yes -o "$enable_web_ide" = yes; then
141+
else
142+
found_mlmpfr=yes
143+
AC_MSG_CHECKING([for mlmpfr])
144+
- DIR=$($OCAMLFIND query mlmpfr 2> /dev/null)
145+
+ DIR=$($OCAMLFIND query mlmpfr | tr -d '\r' 2> /dev/null)
146+
if test -n "$DIR"; then
147+
AC_MSG_RESULT([yes])
148+
old_mpfr=no
149+
echo "ocamlfind found mlmpfr in $DIR"
150+
# Test that MPFR version is higher than 4.0.0 (because of
151+
# Faithful constructor incompatibility).
152+
- MPFRVERSION=$($OCAMLFIND query -format "%v" mlmpfr 2> /dev/null)
153+
+ MPFRVERSION=$($OCAMLFIND query -format "%v" mlmpfr | tr -d '\r' 2> /dev/null)
154+
AX_VERSION_GE([$MPFRVERSION], 4.0.0, [], [
155+
found_mlmpfr=no
156+
reason_mpfr=" (mlmpfr >= 4.0.0 not found)"])
157+
@@ -848,7 +848,7 @@ else
158+
found_js_of_ocaml=yes
159+
for p in js_of_ocaml js_of_ocaml-ppx; do
160+
AC_MSG_CHECKING([for $p])
161+
- DIR=$($OCAMLFIND query $p 2> /dev/null)
162+
+ DIR=$($OCAMLFIND query $p | tr -d '\r' 2> /dev/null)
163+
if test -z "$DIR"; then
164+
AC_MSG_RESULT([no])
165+
found_js_of_ocaml=no
166+
@@ -891,7 +891,7 @@ if test "$enable_statmemprof" = yes; then
167+
enable_statmemprof=no
168+
reason_statmemprof=" (ocamlfind not available)"
169+
else
170+
- DIR=$($OCAMLFIND query statmemprof-emacs 2> /dev/null)
171+
+ DIR=$($OCAMLFIND query statmemprof-emacs | tr -d '\r' 2> /dev/null)
172+
if test -z "$DIR"; then
173+
enable_statmemprof=no
174+
reason_statmemprof=" (statmemprof-emacs not found)"
175+
@@ -915,7 +915,7 @@ else
176+
else
177+
for p in ppx_sexp_conv sexplib ppx_deriving; do
178+
AC_MSG_CHECKING([for $p using ocamlfind])
179+
- DIR=$($OCAMLFIND query $p 2> /dev/null)
180+
+ DIR=$($OCAMLFIND query $p | tr -d '\r' 2> /dev/null)
181+
if test -z "$DIR"; then
182+
AC_MSG_RESULT([no])
183+
enable_pp_sexp=no

‎packages/why3/why3.1.6.0/opam‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,8 @@ conflicts: [
7676
"base-effects"
7777
]
7878

79+
patches: [ "cygwin.patch" { os-family = "windows" } ]
80+
7981
synopsis: "Why3 environment for deductive program verification"
8082

8183
description: """

0 commit comments

Comments
 (0)