abella
abella copied to clipboard
abella-prover
Support bytecode-only target for 32-bit platforms like powerpc
While 2.0.7 built fine (after fixing bytecode target), 2.0.8 fails now:
---> Building abella
Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8" && /usr/bin/make -j6 -w all
make: Entering directory `/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8'
dune build src/abella.exe src/abella_doc.exe src/abella_dep.exe
File "src/lexer.mll", line 1, character 0: syntax error.
File "src/parser.mly", line 1, characters 0-0:
Error: syntax error inside a declaration.
Did you perhaps forget the %% that separates declarations and rules?
make: *** [all] Error 1
The log has:
# dune build src/abella.exe src/abella_doc.exe src/abella_dep.exe
# OCAMLPARAM: unset
# Shared cache: disabled
# Workspace root:
# /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8
# Auto-detected concurrency: 4
$ /opt/local/bin/ocamlc -config > /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/.tmp/dune_17ef15_output
# Dune context:
# { name = "default"
# ; kind = "default"
# ; profile = Dev
# ; merlin = true
# ; for_host = None
# ; fdo_target_exe = None
# ; build_dir = In_build_dir "default"
# ; ocaml_bin = External "/opt/local/bin"
# ; ocaml = Ok External "/opt/local/bin/ocaml"
# ; ocamlc = External "/opt/local/bin/ocamlc"
# ; ocamlopt =
# Error
# { context = "default"
# ; program = "ocamlopt"
# ; hint =
# Some
# "ocamlc found in /opt/local/bin, but /opt/local/bin/ocamlopt doesn't exist (context: default)"
# }
# ; ocamldep = Ok External "/opt/local/bin/ocamldep"
# ; ocamlmklib = Ok External "/opt/local/bin/ocamlmklib"
# ; installed_env =
# map
# { "INSIDE_DUNE" :
# "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8/_build/default"
# }
# ; findlib_paths = [ External "/opt/local/lib/ocaml/site-lib" ]
# ; ocaml_config =
# { version = "4.14.1"
# ; standard_library_default = "/opt/local/lib/ocaml"
# ; standard_library = "/opt/local/lib/ocaml"
# ; standard_runtime = "the_standard_runtime_variable_was_deleted"
# ; ccomp_type = "cc"
# ; c_compiler = "/opt/local/bin/gcc-mp-13"
# ; ocamlc_cflags =
# [ "-arch"
# ; "ppc"
# ; "-O2"
# ; "-fno-strict-aliasing"
# ; "-fwrapv"
# ; "-pthread"
# ; "-pipe"
# ; "-Os"
# ; "-arch"
# ; "ppc"
# ]
# ; ocamlc_cppflags =
# [ "-arch"; "ppc"; "-D_FILE_OFFSET_BITS=64"; "-I/opt/local/include" ]
# ; ocamlopt_cflags =
# [ "-arch"
# ; "ppc"
# ; "-O2"
# ; "-fno-strict-aliasing"
# ; "-fwrapv"
# ; "-pthread"
# ; "-pipe"
# ; "-Os"
# ; "-arch"
# ; "ppc"
# ]
# ; ocamlopt_cppflags =
# [ "-arch"; "ppc"; "-D_FILE_OFFSET_BITS=64"; "-I/opt/local/include" ]
# ; bytecomp_c_compiler =
# [ "/opt/local/bin/gcc-mp-13"
# ; "-arch"
# ; "ppc"
# ; "-O2"
# ; "-fno-strict-aliasing"
# ; "-fwrapv"
# ; "-pthread"
# ; "-pipe"
# ; "-Os"
# ; "-arch"
# ; "ppc"
# ; "-D_FILE_OFFSET_BITS=64"
# ; "-I/opt/local/include"
# ]
# ; bytecomp_c_libraries = [ "-lm"; "-lpthread" ]
# ; native_c_compiler =
# [ "/opt/local/bin/gcc-mp-13"
# ; "-arch"
# ; "ppc"
# ; "-O2"
# ; "-fno-strict-aliasing"
# ; "-fwrapv"
# ; "-pthread"
# ; "-pipe"
# ; "-Os"
# ; "-arch"
# ; "ppc"
# ; "-D_FILE_OFFSET_BITS=64"
# ; "-I/opt/local/include"
# ]
# ; native_c_libraries = [ "-lm" ]
# ; native_pack_linker =
# [ "/opt/local/bin/gcc-mp-13"; "-arch"; "ppc"; "-Wl,-r"; "-o" ]
# ; cc_profile = []
# ; architecture = "power"
# ; model = "ppc"
# ; int_size = 31
# ; word_size = 32
# ; system = "rhapsody"
# ; asm =
# [ "/opt/local/bin/gcc-mp-13"
# ; "-arch"
# ; "ppc"
# ; "-Wno-trigraphs"
# ; "-c"
# ]
# ; asm_cfi_supported = false
# ; with_frame_pointers = false
# ; ext_exe = ""
# ; ext_obj = ".o"
# ; ext_asm = ".s"
# ; ext_lib = ".a"
# ; ext_dll = ".so"
# ; os_type = "Unix"
# ; default_executable_name = "a.out"
# ; systhread_supported = true
# ; host = "powerpc-apple-darwin10.0.0d2"
# ; target = "powerpc-apple-darwin10.0.0d2"
# ; profiling = false
# ; flambda = false
# ; spacetime = false
# ; safe_string = true
# ; exec_magic_number = "Caml1999X031"
# ; cmi_magic_number = "Caml1999I031"
# ; cmo_magic_number = "Caml1999O031"
# ; cma_magic_number = "Caml1999A031"
# ; cmx_magic_number = "Caml1999Y031"
# ; cmxa_magic_number = "Caml1999Z031"
# ; ast_impl_magic_number = "Caml1999M031"
# ; ast_intf_magic_number = "Caml1999N031"
# ; cmxs_magic_number = "Caml1999D031"
# ; cmt_magic_number = "Caml1999T031"
# ; natdynlink_supported = false
# ; supports_shared_libraries = true
# ; windows_unicode = false
# }
# ; instrument_with = []
# }
. . .
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/version.ml) > _build/default/src/.abella_lib.objs/version.impl.d
$ (cd _build/default && /opt/local/bin/ocamllex -q -o src/lexer.ml src/lexer.mll)
> File "src/lexer.mll", line 1, character 0: syntax error.
[3]
. . .
$ (cd _build/.sandbox/ffc46ec10f56917b72165f6a014501b3/default && /opt/local/bin/menhir --explain src/parser.mly --base src/parser --infer-write-query src/parser__mock.ml.mock)
> File "src/parser.mly", line 1, characters 0-0:
> Error: syntax error inside a declaration.
> Did you perhaps forget the %% that separates declarations and rules?
[1]
What is going wrong?
It seems like your OCaml installation is broken. This is clearly not a problem at Abella's end since our CI builds and tests Abella on every commit. Can you check if you can independently run ocamllex and menhir?
@chaudhuri I will try once on a desktop, but I think they work, since I build multiple OCaml ports, including stanc3 compiler, which does use at least menhir.
To be clear, it is supposed to work with bytecode compilation, right? 2.0.7 did not, but a fix for it was rather minimal: https://github.com/macports/macports-ports/commit/682b78e9d8be9ffeef37fc8c85086f84fe31cd6e (see the patching there).
I can't think of why byte compilation would fail. Abella is currently 100% ocaml. I'll look into adding powerpc to our CI and see if any errors are reported. I don't personally have a powerpc (or even a Mac) to do any direct testing though.
I can't think of why byte compilation would fail. Abella is currently 100% ocaml. I'll look into adding powerpc to our CI and see if any errors are reported. I don't personally have a powerpc (or even a Mac) to do any direct testing though.
Another thing I could think of, which makes our PowerPC setup a bit specific, is this setting in Dune: https://github.com/macports/macports-ports/blob/4e35e8abb053882dc163a85cafcdef38465c0562/ocaml/ocaml-dune/Portfile#L35 (there is a link to a discussion with upstream too).
I will try a few things tomorrow: Update Dune to 3.12.1 and see if nothing changes. Try rebuilding all OCaml dependencies of Abella from scratch (if Opam is in the chain somewhere, that could be a complication, there is some bug in it, but hopefully fixable). Try building 2.0.8 on aarch64 to make sure the problem is specific to either PowerPC or 32-bit and not to our set-up of the build as such.
Unfortunately I can't find a public CI runner that matches your configuration (arch=ppc32,os=macos). If you know of one, or even some place where I can do some testing on my own, please let me know.
Unrelatedly, I've verified that a byte-compiled version of Abella builds and runs without issues on arch=x86_64,os={linux,windows} and arch=arm64,os=macos. These are the only systems I have access to either through my own computers or through the CI runner.
@chaudhuri I do not think that macOS ppc will be available via GH actions or alike; while it is feasible to emulate (install 10.6.8 Server in VM, run ppc code via Rosetta; or install 10.5.8 ppc in Qemu), it is likely to be a pain, especially given that everything will have to be built from scratch there. Realistically, Linux ppc32 may be the closest to test on (ABI is not identical, but bitness, arch and endianness are).
@chaudhuri I have rebuilt OCaml and updated dune to 3.12.1, same error. Just to be clear, abella 2.0.8 has been tested with OCaml 4.14.1?
I use 4.14.1 to develop Abella.
Unfortunately, I can't think of any reason why this is failing. Can you get the sources from the release and run ocamllex on src/lexer.mll and menhir on src/parser.mly? Let me know what errors you get.
36-184% /opt/local/bin/ocamllex /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8/src/lexer.mll
67 states, 773 transitions, table size 3494 bytes
1797 additional bytes used for bindings
36-184% /opt/local/bin/menhir /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8/src/parser.mly
Warning: one state has shift/reduce conflicts.
Warning: one shift/reduce conflict was arbitrarily resolved.
Error: the code back-end requires the type of every nonterminal symbol to be
known. Please specify the type of every symbol via %type declarations, or
enable type inference (look up --infer in the manual).
Type inference is automatically enabled when Menhir is used via Dune,
provided the dune-project file says (using menhir 2.0) or later.
The types of the following nonterminal symbols are unknown:
aid
any_command
apply_arg
aty
binder
binding_list
binding_one
binding_vars
boption(STAR)
boption(__anonymous_6)
clause
clause_body
clause_head
clause_name
clause_sel
clearable
cmdline_flag
command
common_command
context
contexted_term
def
depth_spec_one
ewitness
exists_binds
exp
exp_list
focused_term
hyp
id
id_tys
knd
list(__anonymous_0)
list(__anonymous_1)
list(located(sig_decl))
list(mod_clause)
list(sig_decl)
loc_id
loption(__anonymous_13)
loption(__anonymous_14)
loption(__anonymous_16)
loption(__anonymous_2)
loption(__anonymous_3)
loption(__anonymous_4)
loption(__anonymous_5)
loption(exp_list)
loption(hyp_list)
loption(separated_nonempty_list(COMMA,cmdline_flag))
maybe_depth
nonempty_list(NUM)
nonempty_list(__anonymous_10)
nonempty_list(__anonymous_11)
nonempty_list(__anonymous_8)
nonempty_list(__anonymous_9)
nonempty_list(apply_arg)
nonempty_list(binding_one)
nonempty_list(hyp)
nonempty_list(id)
objseq
option(NUM)
option(SEMICOLON)
option(hyp)
paid
pty
pure_command
pure_top_command
restriction
separated_nonempty_list(COMMA,__anonymous_12)
separated_nonempty_list(COMMA,__anonymous_15)
separated_nonempty_list(COMMA,__anonymous_7)
separated_nonempty_list(COMMA,aty)
separated_nonempty_list(COMMA,cmdline_flag)
separated_nonempty_list(COMMA,ewitness)
separated_nonempty_list(COMMA,loc_id)
separated_nonempty_list(COMMA,search_witness)
separated_nonempty_list(COMMA,uty)
separated_nonempty_list(SEMICOLON,def)
separated_nonempty_list(SEMICOLON,depth_spec_one)
sol_sel
theorem_typarams
top_command
ty
uty
Looks like both ocamllex and menhir worked fine. (The menhir error can be suppressed with --infer.)
Hmm...
Maybe Dune's _build directory is broken on ppc32 somehow? What do you get when you run the exact command in the initial message:
$ cd /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8/
$ dune build src/abella.exe # which may fail, but that's OK because:
$ (cd _build/default && /opt/local/bin/ocamllex -q -o src/lexer.ml src/lexer.mll)
By the way, one weird thing is that you are trying to build a .exe target, which normally invokes ocamlopt (the native compiler). If you want to byte-compile, then you have to change the extensions to .bc in the Makefile, and also add (modes byte exe) to the executables section in src/dune. If you want, I can give you a patch against the v2.0.8 tag that will change to build Abella in byte compiled mode.
@chaudhuri
If you want, I can give you a patch against the v2.0.8 tag that will change to build Abella in byte compiled mode.
Yes, please, that would be great. For 2.0.7 I had to fix bytecode target for it to work. But it is much better to have a proper fix from you rather than making a guesswork on our end.
Native compiler is broken for ppc, and given that OCaml upstream dropped 32-bit support in native compiler in OCaml 5, I gave up on a work to fix it. (One thing was to fix ABI for macOS, when Linux was supported, but restoring support for 32-bit will be too much.) So most likely we are stuck with bytecode.
(ppc64 on macOS too, since assembler and ABI will need changes, and there is little sense to do that for the sake of ppc64 alone.)
By the way, could you say if the following error looks related? https://trac.macports.org/ticket/68586#comment:1
Maybe there is some problem with dune which affects select ports (since most of dependents build fine, but opam now fails).
This is running directly after unpacking the source:
36-184% cd /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8
36-184% sudo dune build src/abella.exe
File "src/lexer.mll", line 1, character 0: syntax error.
File "src/parser.mly", line 1, characters 0-0:
Error: syntax error inside a declaration.
Did you perhaps forget the %% that separates declarations and rules?
36-184% cd /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-2.0.8/_build/default
36-184% sudo /opt/local/bin/ocamllex -q -o src/lexer.ml src/lexer.mll
File "src/lexer.mll", line 1, character 0: syntax error.
Right, so what's the file in _build/default/src/lexer.mll? It should be identical to src/lexer.mll.
Check out a10b8e7435eacf44f44db92230daeee09533f072 (tag v2.0.8+bc) for a byte-compiled version of the Abella distribution. Very lightly tested with just make test on my system (x86_64-linux-debian), but at least it successfully checks the standard examples shipped with Abella.
Unfortunately, I still get the same failure with syntax when building from a10b8e7435eacf44f44db92230daeee09533f072 commit:
---> Building abella
Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072" && /usr/bin/make -j6 -w all
make: Entering directory `/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072'
dune build src/abella.bc src/abella_doc.bc src/abella_dep.bc
File "src/lexer.mll", line 1, character 0: syntax error.
File "src/parser.mly", line 1, characters 0-0:
Error: syntax error inside a declaration.
Did you perhaps forget the %% that separates declarations and rules?
make: *** [all] Error 1
make: Leaving directory `/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072'
Command failed: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072" && /usr/bin/make -j6 -w all
Exit code: 2
@chaudhuri If I understood correctly what to run, _build/default/src/lexer.mll file is empty and shows as 0 bytes.
Here is what I did after unpacking. No Macports involvement here besides fetching from git and extracting:
36-141% cd /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072
36-141% sudo dune build src/abella.bc
Password:
File "src/lexer.mll", line 1, character 0: syntax error.
File "src/parser.mly", line 1, characters 0-0:
Error: syntax error inside a declaration.
Did you perhaps forget the %% that separates declarations and rules?
36-141% cd /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072/_build/default/
36-141% sudo /opt/local/bin/ocamllex -q -o src/lexer.ml src/lexer.mll
File "src/lexer.mll", line 1, character 0: syntax error.
If I did something silly, please tell me what commands to run manually to get a needed output.
OK, this is then not an Abella issue at all. It appears that Dune is not making the _build directory correctly. Please file an issue with https://github.com/ocaml/dune/issues.
@chaudhuri Your hint about _build dir helped me to figure out what was going wrong. Since abella uses makefile and not dune directly, DUNE_CONFIG__COPY_FILE=portable did not get passed in the environment, and I forgot about that being needed. I added it now manually, and the build can start.
Where does it put the binary now though? It certainly did quite a bit, but I do not see abella binary:
# dune build src/abella.bc src/abella_doc.bc src/abella_dep.bc
# OCAMLPARAM: unset
# Shared cache: disabled
# Shared cache location:
# /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/.home/.cache/dune/db
# Workspace root:
# /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072
# Auto-detected concurrency: 4
# Dune context:
# { name = "default"
# ; kind = "default"
# ; profile = Dev
# ; merlin = true
# ; fdo_target_exe = None
# ; build_dir = In_build_dir "default"
# ; installed_env =
# map
# { "INSIDE_DUNE" :
# "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/abella-a10b8e7435eacf44f44db92230daeee09533f072/_build/default"
# }
# ; instrument_with = []
# }
$ /opt/local/bin/ocamlc -config > /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_abella/abella/work/.tmp/dune_51d661_output
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/version.ml) > _build/default/src/.abella_lib.objs/version.impl.d
$ (cd _build/default && /opt/local/bin/ocamllex -q -o src/lexer.ml src/lexer.mll)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/version.cmo -c -impl src/version.ml)
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/abella_doc_dist.ml) > _build/default/src/.abella_lib.objs/abella_doc_dist.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/abella_types.ml) > _build/default/src/.abella_lib.objs/abella_types.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/accumulate.ml) > _build/default/src/.abella_lib.objs/accumulate.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/checks.ml) > _build/default/src/.abella_lib.objs/checks.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/context.ml) > _build/default/src/.abella_lib.objs/context.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/depend.ml) > _build/default/src/.abella_lib.objs/depend.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/filepath.ml) > _build/default/src/.abella_lib.objs/filepath.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/graph.ml) > _build/default/src/.abella_lib.objs/graph.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/extensions.ml) > _build/default/src/.abella_lib.objs/extensions.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/output.ml) > _build/default/src/.abella_lib.objs/output.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/pretty.ml) > _build/default/src/.abella_lib.objs/pretty.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/state.ml) > _build/default/src/.abella_lib.objs/state.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/subordination.ml) > _build/default/src/.abella_lib.objs/subordination.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/metaterm.ml) > _build/default/src/.abella_lib.objs/metaterm.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/prover.ml) > _build/default/src/.abella_lib.objs/prover.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/typing.ml) > _build/default/src/.abella_lib.objs/typing.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/term.ml) > _build/default/src/.abella_lib.objs/term.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/unify.ml) > _build/default/src/.abella_lib.objs/unify.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/unifyty.ml) > _build/default/src/.abella_lib.objs/unifyty.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/tactics.ml) > _build/default/src/.abella_lib.objs/tactics.impl.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/graph.mli) > _build/default/src/.abella_lib.objs/graph.intf.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/pretty.mli) > _build/default/src/.abella_lib.objs/pretty.intf.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/state.mli) > _build/default/src/.abella_lib.objs/state.intf.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/subordination.mli) > _build/default/src/.abella_lib.objs/subordination.intf.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/term.mli) > _build/default/src/.abella_lib.objs/term.intf.d
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/unify.mli) > _build/default/src/.abella_lib.objs/unify.intf.d
$ (cd _build/.sandbox/a267c9c056edfedf8682cb97714be6b2/default && /opt/local/bin/menhir --explain src/parser.mly --base src/parser --infer-write-query src/parser__mock.ml.mock)
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/lexer.ml) > _build/default/src/.abella_lib.objs/lexer.impl.d
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/abella_doc_dist.cmo -c -impl src/abella_doc_dist.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/state.cmi -c -intf src/state.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/pretty.cmi -c -intf src/pretty.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/term.cmi -c -intf src/term.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/pretty.cmo -c -impl src/pretty.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/graph.cmi -c -intf src/graph.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/subordination.cmi -c -intf src/subordination.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/unifyty.cmo -c -impl src/unifyty.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/unify.cmi -c -intf src/unify.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/extensions.cmo -c -impl src/extensions.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/filepath.cmo -c -impl src/filepath.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/state.cmo -c -impl src/state.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/output.cmo -c -impl src/output.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/graph.cmo -c -impl src/graph.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/subordination.cmo -c -impl src/subordination.ml)
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/parser__mock.ml.mock) > _build/default/src/.abella_lib.objs/parser__mock.impl.d
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/context.cmo -c -impl src/context.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/term.cmo -c -impl src/term.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/unify.cmo -c -impl src/unify.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/metaterm.cmo -c -impl src/metaterm.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/typing.cmo -c -impl src/typing.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/abella_types.cmo -c -impl src/abella_types.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/checks.cmo -c -impl src/checks.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/tactics.cmo -c -impl src/tactics.ml)
$ (cd _build/.sandbox/7bcfc159da2d83edcf8b17ac11240a10/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -short-paths -i -impl src/parser__mock.ml.mock) > _build/.sandbox/7bcfc159da2d83edcf8b17ac11240a10/default/src/parser__mock.mli.inferred
$ (cd _build/.sandbox/cb5d3ad1817f5e827e1a726ddc64e7bc/default && /opt/local/bin/menhir --explain src/parser.mly --base src/parser --infer-read-reply src/parser__mock.mli.inferred)
> Warning: one state has shift/reduce conflicts.
> Warning: one shift/reduce conflict was arbitrarily resolved.
$ (cd _build/default && /opt/local/bin/ocamldep -modules -intf src/parser.mli) > _build/default/src/.abella_lib.objs/parser.intf.d
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/parser.cmi -c -intf src/parser.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/lexer.cmo -c -impl src/lexer.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/accumulate.cmo -c -impl src/accumulate.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/depend.cmo -c -impl src/depend.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -no-alias-deps -opaque -o src/.abella_lib.objs/byte/prover.cmo -c -impl src/prover.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella.eobjs/byte -I /opt/local/lib/ocaml/site-lib/cmdliner -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -I src/.abella_lib.objs/byte -no-alias-deps -opaque -o src/.abella.eobjs/byte/dune__exe__Abella.cmi -c -intf src/abella.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_doc.eobjs/byte -I /opt/local/lib/ocaml/site-lib/cmdliner -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -I src/.abella_lib.objs/byte -no-alias-deps -opaque -o src/.abella_doc.eobjs/byte/dune__exe__Abella_doc.cmi -c -intf src/abella_doc.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_dep.eobjs/byte -I /opt/local/lib/ocaml/site-lib/cmdliner -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -I src/.abella_lib.objs/byte -no-alias-deps -opaque -o src/.abella_dep.eobjs/byte/dune__exe__Abella_dep.cmi -c -intf src/abella_dep.mli)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_dep.eobjs/byte -I /opt/local/lib/ocaml/site-lib/cmdliner -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -I src/.abella_lib.objs/byte -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_dep.eobjs/byte/dune__exe__Abella_dep.cmo -c -impl src/abella_dep.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_doc.eobjs/byte -I /opt/local/lib/ocaml/site-lib/cmdliner -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -I src/.abella_lib.objs/byte -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_doc.eobjs/byte/dune__exe__Abella_doc.cmo -c -impl src/abella_doc.ml)
$ (cd _build/default && /opt/local/bin/ocamldep -modules -impl src/parser.ml) > _build/default/src/.abella_lib.objs/parser.impl.d
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella.eobjs/byte -I /opt/local/lib/ocaml/site-lib/cmdliner -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -I src/.abella_lib.objs/byte -intf-suffix .ml -no-alias-deps -opaque -o src/.abella.eobjs/byte/dune__exe__Abella.cmo -c -impl src/abella.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -bin-annot -I src/.abella_lib.objs/byte -I /opt/local/lib/ocaml/site-lib/seq -I /opt/local/lib/ocaml/site-lib/yojson -intf-suffix .ml -no-alias-deps -opaque -o src/.abella_lib.objs/byte/parser.cmo -c -impl src/parser.ml)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -a -o src/abella_lib.cma src/.abella_lib.objs/byte/version.cmo src/.abella_lib.objs/byte/pretty.cmo src/.abella_lib.objs/byte/extensions.cmo src/.abella_lib.objs/byte/state.cmo src/.abella_lib.objs/byte/term.cmo src/.abella_lib.objs/byte/unifyty.cmo src/.abella_lib.objs/byte/graph.cmo src/.abella_lib.objs/byte/subordination.cmo src/.abella_lib.objs/byte/unify.cmo src/.abella_lib.objs/byte/context.cmo src/.abella_lib.objs/byte/metaterm.cmo src/.abella_lib.objs/byte/typing.cmo src/.abella_lib.objs/byte/abella_types.cmo src/.abella_lib.objs/byte/tactics.cmo src/.abella_lib.objs/byte/output.cmo src/.abella_lib.objs/byte/checks.cmo src/.abella_lib.objs/byte/parser.cmo src/.abella_lib.objs/byte/lexer.cmo src/.abella_lib.objs/byte/prover.cmo src/.abella_lib.objs/byte/filepath.cmo src/.abella_lib.objs/byte/accumulate.cmo src/.abella_lib.objs/byte/depend.cmo src/.abella_lib.objs/byte/abella_doc_dist.cmo)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -o src/abella_dep.bc /opt/local/lib/ocaml/site-lib/seq/seq.cma /opt/local/lib/ocaml/site-lib/yojson/yojson.cma src/abella_lib.cma /opt/local/lib/ocaml/unix.cma /opt/local/lib/ocaml/site-lib/cmdliner/cmdliner.cma src/.abella_dep.eobjs/byte/dune__exe__Abella_dep.cmo)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -o src/abella.bc /opt/local/lib/ocaml/site-lib/seq/seq.cma /opt/local/lib/ocaml/site-lib/yojson/yojson.cma src/abella_lib.cma /opt/local/lib/ocaml/unix.cma /opt/local/lib/ocaml/site-lib/cmdliner/cmdliner.cma src/.abella.eobjs/byte/dune__exe__Abella.cmo)
$ (cd _build/default && /opt/local/bin/ocamlc -w @[email protected]@30..39@[email protected]@[email protected]@67@69-40 -strict-sequence -strict-formats -short-paths -keep-locs -g -o src/abella_doc.bc /opt/local/lib/ocaml/site-lib/seq/seq.cma /opt/local/lib/ocaml/site-lib/yojson/yojson.cma src/abella_lib.cma /opt/local/lib/ocaml/unix.cma /opt/local/lib/ocaml/site-lib/cmdliner/cmdliner.cma src/.abella_doc.eobjs/byte/dune__exe__Abella_doc.cmo)
P. S. If we could have bytecode target in the master branch (not as a default one, of course, but just available to be chosen), it would be great.
If you run make all-release abella.install, it will create a file called abella.install that has instructions for all the files that need to be installed. The format of the file should be fairly obvious.
P. S. If we could have bytecode target in the master branch (not as a default one, of course, but just available to be chosen), it would be great.
I agree, but unfortunately I am leaving for winter break in a few hours until the end of the year. It will have to happen in the 2.0.9 bugfix release, probably out in early February.
@chaudhuri Got it. Until then I can make a local patch for Macports.
Thank you very much for your help here. (And sorry that it took so long – I should have remembered that this variable is needed in the environment, not just in Dune itself.)
Sorry for the delays. Can you check if the 2.0.8.2 release compiles for you out of the box? The DUNE variable in the Makefile can be tweaked as needed for your own version of Dune, but otherwise OPAM should automatically switch to bytecode for arch=ppc32|ppc64. If you're not using OPAM to build, you would have to also set the BYTECODE environment variable to some non-empty string such as true.
The following might possibly work for your case:
$ make BYTECODE=true DUNE="DUNE_CONFIG__COPY_FILE=portable dune" all-release abella.install