From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <gbuday@gmail.com>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id C273D81792
	for <caml-list@sympa.inria.fr>; Tue, 18 Jun 2013 15:18:38 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  gbuday@gmail.com) identity=pra; client-ip=209.85.219.49;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="gbuday@gmail.com";
  x-sender="gbuday@gmail.com"; x-conformance=sidf_compatible
Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of
  gbuday@gmail.com designates 209.85.219.49 as permitted
  sender) identity=mailfrom; client-ip=209.85.219.49;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="gbuday@gmail.com";
  x-sender="gbuday@gmail.com"; x-conformance=sidf_compatible;
  x-record-type="v=spf1"
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-oa0-f49.google.com) identity=helo;
  client-ip=209.85.219.49;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="gbuday@gmail.com";
  x-sender="postmaster@mail-oa0-f49.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Aq0BAPZcwFHRVdsxlGdsb2JhbABZgzpJwAMIFg4BAQEBBwsLCRIqgmoBGw8PAxIQXQERAQUBBhCIGgEDD5oTgn6MS4J/hFQKGScNWId0AQUMj0yDSwOXQY9eFimENzo
X-IPAS-Result: Aq0BAPZcwFHRVdsxlGdsb2JhbABZgzpJwAMIFg4BAQEBBwsLCRIqgmoBGw8PAxIQXQERAQUBBhCIGgEDD5oTgn6MS4J/hFQKGScNWId0AQUMj0yDSwOXQY9eFimENzo
X-IronPort-AV: E=Sophos;i="4.87,889,1363129200"; 
   d="scan'208";a="18166417"
Received: from mail-oa0-f49.google.com ([209.85.219.49])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 18 Jun 2013 15:18:38 +0200
Received: by mail-oa0-f49.google.com with SMTP id n9so4906138oag.22
        for <caml-list@inria.fr>; Tue, 18 Jun 2013 06:18:36 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:date:message-id:subject:from:to:content-type;
        bh=w7pVkLEYXYP76qc3n6IgAY9TWdKERNyCzuydKAkvQnc=;
        b=wgJKUzlomTQ24ZAXfzq0kiIgzBMKMBM7+AYRlHsNHRVWQq8FxjCeYBm2ZtOcsQ9aZM
         PxBSeEp6+L8GLynYsHdjdu11ihf5P53wOTd8e/v/uOQAE1IYO8selbfgyhjidVT7yav2
         P19Ker9osKvpflHyHcElduLkbSTKUbMXXf9wOs8+VIJVP5UaefY0+LOrrWTgkGdHhKwm
         Rpkux3QExXUWa6fUlSYBYgnLdJesuPitN9slAywsJ6qhADaIMY22zTpo/FezhNe+p+Iy
         RP76tZEhnx7+SKNwF2HknLgZc1HnY/Cp8+tLzQ9Jhv2Ki14RdX1ToBIEWI4nMMDLL3FK
         YGtg==
MIME-Version: 1.0
X-Received: by 10.60.174.111 with SMTP id br15mr11811514oec.130.1371561516776;
 Tue, 18 Jun 2013 06:18:36 -0700 (PDT)
Received: by 10.76.35.35 with HTTP; Tue, 18 Jun 2013 06:18:36 -0700 (PDT)
Date: Tue, 18 Jun 2013 15:18:36 +0200
Message-ID: <CA+3iOzks0bHbp4eKuxtTqyMAuTxbmyPnYmXsHb-b4KAWEjdh4w@mail.gmail.com>
From: Gergely Buday <gbuday@gmail.com>
To: caml-list@inria.fr
Content-Type: text/plain; charset=ISO-8859-1
Subject: [Caml-list] using ocamlc

Hi there,

I want to use ocaml as a compiler for the LEO-II theorem prover. I
guess the following error should tell more to OCaml experts than to
the author of the prover:

$ make
ocamlc  -g -I ./calculus/ -I ./datastructure/ -I ./general/ -I
./interfaces/ -I ./interfaces/minisat/ -I ./interfaces/translation/ -I
./parser-hotptp/ -I ./toplevel/ unix.cma str.cma
/home/gergoe/local/leo2/src/interfaces/minisat/dllminisatinterface.so
 -pp "camlp4o.opt Camlp4MacroParser.cmxs -DDEBUG " -c
datastructure/darray.mli
Camlp4: Uncaught exception: DynLoader.Error
("./Camlp4MacroParser.cmxs", "error loading shared library:
./Camlp4MacroParser.cmxs: undefined symbol: camlList__combine_254")

File "datastructure/darray.mli", line 1:
Error: Preprocessor error
make: *** [datastructure/darray.cmi] Error 2

I have the version

$ ocamlc -version
4.00.1

What is missing here? I installed OCaml first from yum repository on
my CentOS box, but LEO-II needs OCaml 4.00 so I installed it from
source.

The mentioned cmxs file is in the directory where I call make:

$ find ~/local/ -name Camlp4MacroParser.cmxs
/home/gergoe/local/leo2/src/Camlp4MacroParser.cmxs

- Gergely