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
121
|
From: =?utf-8?q?St=C3=A9phane_Glondu?= <glondu@debian.org>
Date: Mon, 14 Oct 2024 11:01:34 +0200
Subject: Fix build on bytecode architectures
Bug-Debian: https://bugs.debian.org/1084815
---
Makefile | 8 +++++---
ocaml-lib/ocamlbuild.mk | 11 +++++++++--
src/Makefile | 6 ++++--
src/_tags | 1 +
4 files changed, 19 insertions(+), 7 deletions(-)
diff --git a/Makefile b/Makefile
index 9f72c73..214b7d7 100644
--- a/Makefile
+++ b/Makefile
@@ -9,6 +9,8 @@ DDIR=lem-$(LEMVERSION)
#INSTALL_DIR := $(realpath .)
INSTALL_DIR := $(DESTDIR)
+OCAMLBUILD_BEST ?= native
+
#all: il.pdf build-main ilTheory.uo
all: bin/lem libs_phase_1
@@ -17,7 +19,7 @@ all: bin/lem libs_phase_1
install:
mkdir -p $(INSTALL_DIR)/bin
rm -f $(INSTALL_DIR)/bin/lem
- cp src/main.native $(INSTALL_DIR)/bin/lem
+ cp src/main.$(OCAMLBUILD_BEST) $(INSTALL_DIR)/bin/lem
rm -rf $(INSTALL_DIR)/share/lem
mkdir -p $(INSTALL_DIR)/share/lem/library
cp library/*.lem $(INSTALL_DIR)/share/lem/library
@@ -179,7 +181,7 @@ debug: version share_directory
build-lem: version share_directory
$(MAKE) -C src all
- ln -sf src/main.native lem
+ ln -sf src/main.$(OCAMLBUILD_BEST) lem
build-lem-profile: version share_directory
$(MAKE) -C src profile
@@ -190,7 +192,7 @@ lem: build-lem
bin/lem: lem
mkdir -p bin
- cd bin && ln -sf ../src/main.native lem
+ cd bin && ln -sf ../src/main.$(OCAMLBUILD_BEST) lem
OCAML-LIB-NON_LGPL = \
ocaml-lib/Makefile \
diff --git a/ocaml-lib/ocamlbuild.mk b/ocaml-lib/ocamlbuild.mk
index 1304e0e..626e72a 100644
--- a/ocaml-lib/ocamlbuild.mk
+++ b/ocaml-lib/ocamlbuild.mk
@@ -1,6 +1,13 @@
INSTALLDIR := $(DESTDIR)
LOCALINSTALDIR := local
+OCAMLBUILD_BEST ?= native
+
+ifeq ($(OCAMLBUILD_BEST),native)
+ NATIVE_EXTRACT_TARGET := extract.cmxa
+ NATIVE_EXTRACT_OBJS := _build_%/extract.cmxa _build_%/extract.a
+endif
+
all: extract_zarith extract_num
.PHONY: all
.DEFAULT_GOAL: all
@@ -26,7 +33,7 @@ clean:
extract_zarith extract_num: extract_%:
@ocamlfind query $* > /dev/null || { echo "please install the missing $* package (or do 'make install_dependencies' from `pwd`)" && false; }
- ocamlbuild -build-dir _build_$* -X $(LOCALINSTALDIR) -X dependencies -I num_impl_$* -use-ocamlfind -pkg $* extract.cma extract.cmxa
+ ocamlbuild -build-dir _build_$* -X $(LOCALINSTALDIR) -X dependencies -I num_impl_$* -use-ocamlfind -pkg $* extract.cma $(NATIVE_EXTRACT_TARGET)
.PHONY: extract_zarith extract_num
install_zarith install_num: install_%: extract_%
@@ -37,7 +44,7 @@ uninstall_zarith uninstall_num: uninstall_%:
-ocamlfind remove -destdir $(INSTALLDIR) lem_$*
.PHONY: uninstall_zarith uninstall_num
-$(INSTALLDIR)/lem_zarith/META $(INSTALLDIR)/lem_num/META: $(INSTALLDIR)/lem_%/META: num_impl_%/META _build_%/extract.cma _build_%/extract.cmxa _build_%/extract.a
+$(INSTALLDIR)/lem_zarith/META $(INSTALLDIR)/lem_num/META: $(INSTALLDIR)/lem_%/META: num_impl_%/META _build_%/extract.cma $(NATIVE_EXTRACT_OBJS)
-ocamlfind remove -destdir $(INSTALLDIR) lem_$*
ocamlfind install -destdir $(INSTALLDIR) -patch-version "$(LEMVERSION)" lem_$* $^ `find _build_$* -name '*.cmi' -o -name '*.cmx' -o -name '*.mli'`
touch $@
diff --git a/src/Makefile b/src/Makefile
index a2cc390..4cb50f9 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,5 +1,7 @@
+OCAMLBUILD_BEST ?= native
+
all:
- ocamlbuild -use-ocamlfind -cflags -g main.native
+ ocamlbuild -use-ocamlfind -cflags -g main.$(OCAMLBUILD_BEST)
# ocamlbuild main.native
profile:
@@ -23,7 +25,7 @@ debug:
clean:
-ocamlbuild -clean
- -rm -rf main.native
+ -rm -rf main.$(OCAMLBUILD_BEST)
-rm -rf _build
-rm -rf html-doc
-rm -rf tex-doc
diff --git a/src/_tags b/src/_tags
index 83cae88..1239ecd 100644
--- a/src/_tags
+++ b/src/_tags
@@ -1,5 +1,6 @@
<**/*.ml> : annot, package(zarith)
<**/*.native> : use_str, package(zarith)
+<**/*.byte> : use_str, package(zarith)
<**/*.d.byte> : use_str, package(zarith)
<**/*.mli> : annot, package(zarith)
"ulib" : include
|
