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
122
123
124
125
126
127
128
129
130
131
132
133
|
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 | 20 +++++++++++---------
ocaml-lib/ocamlbuild.mk | 10 ++++++++--
src/Makefile | 6 ++++--
src/_tags | 1 +
4 files changed, 24 insertions(+), 13 deletions(-)
--- a/Makefile
+++ b/Makefile
@@ -9,19 +9,21 @@
#INSTALL_DIR := $(realpath .)
INSTALL_DIR := $(DESTDIR)
+OCAMLBUILD_BEST ?= native
+
#all: il.pdf build-main ilTheory.uo
all: bin/lem libs_phase_1
# we might want run the tests for all backends that are present
install:
- mkdir -p "$(INSTALL_DIR)/bin"
- rm -f "$(INSTALL_DIR)/bin/lem"
- cp src/main.native "$(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"
- cp library/*_constants "$(INSTALL_DIR)/share/lem/library"
+ mkdir -p $(INSTALL_DIR)/bin
+ rm -f $(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
+ cp library/*_constants $(INSTALL_DIR)/share/lem/library
$(MAKE) -C ocaml-lib install
cp -R coq-lib "$(INSTALL_DIR)/share/lem"
cp -R hol-lib "$(INSTALL_DIR)/share/lem"
@@ -179,7 +181,7 @@
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
@@ -191,7 +193,7 @@
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 \
--- 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,12 +33,12 @@
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_%
-ocamlfind remove -destdir "$(INSTALLDIR)" lem_$*
- ocamlfind install -destdir "$(INSTALLDIR)" -patch-version "$(LEMVERSION)" lem_$* num_impl_$*/META _build_$*/extract.cma _build_$*/extract.cmxa _build_$*/extract.a `find _build_$* -name '*.cmi' -o -name '*.cmx' -o -name '*.mli'`
+ ocamlfind install -destdir "$(INSTALLDIR)" -patch-version "$(LEMVERSION)" lem_$* num_impl_$*/META _build_$*/extract.cma $(NATIVE_EXTRACT_OBJS) `find _build_$* -name '*.cmi' -o -name '*.cmx' -o -name '*.mli'`
touch $@
.PHONY: install_zarith install_num
@@ -39,7 +46,6 @@
-ocamlfind remove -destdir "$(INSTALLDIR)" lem_$*
.PHONY: uninstall_zarith uninstall_num
-
install_lem:
-ocamlfind remove -destdir "$(INSTALLDIR)" lem
ocamlfind install -destdir "$(INSTALLDIR)" -patch-version "$(LEMVERSION)" lem META
--- a/src/Makefile
+++ b/src/Makefile
@@ -2,9 +2,11 @@
# Windows with native symlinks appear to clobber an existing
# executable otherwise.
+OCAMLBUILD_BEST ?= native
+
all:
rm -f main.native
- ocamlbuild -use-ocamlfind -cflags -g main.native
+ ocamlbuild -use-ocamlfind -cflags -g main.$(OCAMLBUILD_BEST)
# ocamlbuild main.native
profile:
@@ -28,7 +30,7 @@
clean:
-ocamlbuild -clean
- -rm -rf main.native
+ -rm -rf main.$(OCAMLBUILD_BEST)
-rm -rf _build
-rm -rf html-doc
-rm -rf tex-doc
--- a/src/_tags
+++ b/src/_tags
@@ -1,5 +1,6 @@
<**/*.ml> : annot, bin_annot, package(zarith)
<**/*.native> : use_str, package(zarith)
+<**/*.byte> : use_str, package(zarith)
<**/*.d.byte> : use_str, package(zarith)
<**/*.mli> : annot, bin_annot, package(zarith)
"ulib" : include
|
