Errors in project-everest on FreeBSD

Learning
1

I needed hacl-star support on FreeBSD and managed to build it under project-everest. But I’m stuck trying to build the remainder of project-everest after hitting this error in the quackyducky subproject:

ocamlbuild -tag debug -use-menhir -tag thread -use-ocamlfind -quiet -pkg batteries -pkg menhirLib -pkg fstarlib -pkg process -pkg hacl-star -pkg yojson -cflags -w,-8 Main.native
+ ocamlfind ocamlopt -linkpkg -g -thread -package yojson -package hacl-star -package process -package fstarlib -package menhirLib -package batteries FStar_Getopt.cmx HashingOptions.cmx Hashtable.cmx OS.cmx Version.cmx Options.cmx Ast.cmx Hashing.cmx Batch.cmx Desugar.cmx Binding.cmx BitFields.cmx parser.cmx lexer.cmx ParserDriver.cmx Deps.cmx InlineSingletonRecords.cmx TypeSizes.cmx Simplify.cmx StaticAssertions.cmx Target.cmx Translate.cmx Main.cmx -o Main.native
File "_none_", line 1:
Error: Files Hashing.cmx
   and /usr/home/web/src/vertalo/everest/_opam/lib/ctypes/ctypes.cmxa
   make inconsistent assumptions over interface Ctypes_types
Command exited with code 2.
Hint: Recursive traversal of subdirectories was not enabled for this build,
as the working directory does not look like an ocamlbuild project (no
'_tags' or 'myocamlbuild.ml' file). If you have modules in subdirectories,
you should add the option "-r" or create an empty '_tags' file.

To enable recursive traversal for some subdirectories only, you can use the
following '_tags' file:

  true: -traverse
  <dir1> or <dir2>: traverse

I don’t understand the -traverse option, but imagine that is not the issue if this code builds on other systems. The standard advice for inconsistent interface assumptions seems to be to rebuild the .mli file. I’m using ctypes.0.18.0, and there is no .ml file corresponding to ctypes_types.mli. Can someone point me in the right direction?

2

This error normally happens in dirty builds. If this is a dirty build, try starting from scratch. If it’s a clean build, some of the build rules may be incorrect and randomly/intermittently leading to the error. It’s likely the build rules will need to be fixed.

3

Yes, this kind of errors occurs if some definitions change after .cmi been generated and leads to inconsistency witnessed by the compiler. It does not seem to related to the hint produced by ocamlbuild.

I guess it could be that on FreeBSD the make is not the GNU variant assumed by most building scripts. I think you can try get the gmake installed on FreeBSD, and do some grep and replace to make sure the building script uses the GNU make (or probably just have it override the BSD make in the PATH).

4

This is the result of a clean build in the quackyducky subdirectory. I have build everything from scratch after making the following changes:

  • Clean up some Linuxisms like /bin/bash
  • Add dist/Makefile.tmpl flags in hacl-star to accommodate FreeBSD and build without assembly code
  • Increasing rlimit and rlimit_factor for hacl-star to allow tests to pass
  • Add -thread to the hacl-star build to get past an earlier error in quackyducky
5

Correction: The 3d Makefile does not pass the clean target down to 3d/ocaml, so the 3d/ocaml/_build had not been removed. So the build was not clean. Thanks for the clue! On to the next issue.

1 Like