From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 13BAA7F98F for ; Mon, 31 Jul 2017 18:55:47 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=iguer.auto@gmail.com; spf=Pass smtp.mailfrom=iguer.auto@gmail.com; spf=None smtp.helo=postmaster@mail-wm0-f46.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of iguer.auto@gmail.com) identity=pra; client-ip=74.125.82.46; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="iguer.auto@gmail.com"; x-sender="iguer.auto@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of iguer.auto@gmail.com designates 74.125.82.46 as permitted sender) identity=mailfrom; client-ip=74.125.82.46; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="iguer.auto@gmail.com"; x-sender="iguer.auto@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-wm0-f46.google.com) identity=helo; client-ip=74.125.82.46; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="iguer.auto@gmail.com"; x-sender="postmaster@mail-wm0-f46.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A0n41wh0QwwvYxkXOsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?seIRKvad9pjvdHbS+e9qxAeQG96Ku7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q89pDXYAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+?= =?us-ascii?q?VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfM?= =?us-ascii?q?QA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb5Q6o0WTC/5Kl1ThHmhj?= =?us-ascii?q?oMOzo3/WzXj8B9ir9QrhC8qBxl24PaYJybOuR9cK3Tc9wVSnZOUMlKWixdAI6x?= =?us-ascii?q?dZcDA/YPMOtaqYT2ulsArQG5BQmpHO7hzThIhn/s0q0/zesuDBzN0g8vH9ITrn?= =?us-ascii?q?vUttP1NKMIXuCx1qbD0DLOb/JZ2Tfg9ofIaAotruuRXbJsdsrc0kYvFwbfgVWR?= =?us-ascii?q?rYzpJS+a1uMIs2WC6edrSOyhi2kiqw5rozivwN8hio3IhoITyVDL6zh2wIczJd?= =?us-ascii?q?GiVEF7ZtukHINRtyGVKot5XNkiT3tnuSc6y7wKoZG7fCkWyJQn2h7QcOaLfJSP?= =?us-ascii?q?4hLmUuuaPDR2hGp9db+9iBu+61WsxvP8W8Wu01tGsDBJn9bNu3wV1RHe6NKLRu?= =?us-ascii?q?Zz80u9wzqC2ADe5vtZLU0wl6fWLYMqzKQqmZoJq0vDGzf7mEXog6+ScUUp4u2o?= =?us-ascii?q?5P7mYrXiv5OdOYp0hh3nPqQglcGyAP40MgcJX2ic9uS80KPs8VflT7VNi/06iq?= =?us-ascii?q?jZsJbEKsQHvqO0AQBY3pw+5xqhDzqqytcVkWcdIF9KeR+Ll43pNEvPIPD8A/e/?= =?us-ascii?q?mVOskDJzyvDHMb3hH4vCLmLZnLj7YLZ990lcxRE8zdBa/Z1UC7UBLOjvVU/2sd?= =?us-ascii?q?zUFgU5PBCsw+b7FNV90ZsTVn6VDa+cNKPeqFuI5uM0I+mQf4IVozb8K/095/H0?= =?us-ascii?q?l3M5mFkdfbOo3ZQNcny4EO5mcA2lZi+mid4EFSIOvxEiZO3sklyLFzBJLT7mVK?= =?us-ascii?q?s54nQ/CZm6JYbFXIGkxrKbinSVBJpTM0VBClmJHHugVoqZVu0KbCuWK4c1kzMZ?= =?us-ascii?q?WKLnQpI90jmhsQb7z/xsKe+CqX5Qjo7qyNUgv76brho17zEhVJmQ?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BEDABCYH9Zhi5SfUpbSBgHhAcDgRELA?= =?us-ascii?q?ZxigRg6AQEGBVKJc4xqghIOHoUWAwKECD8YAQEBAQEBAQEBAQESAQEBCAsLCCg?= =?us-ascii?q?kC4IzDIMDFQgBFAceAxIQDwIfBwIlEQEFASINCAEBF4l7AQMIDQQMni2DRT+MC?= =?us-ascii?q?oIEBQEcgwkFg1YKGScNVoMzAQEIAgEdAgYJAQh5gh2DBoIoK4gJgnqCYQWJb41?= =?us-ascii?q?yiA6BaIVnjFhugweHLRGHCpQqM4EVH4FCd3iFDCWBUHSKLwEBAQ?= X-IPAS-Result: =?us-ascii?q?A0BEDABCYH9Zhi5SfUpbSBgHhAcDgRELAZxigRg6AQEGBVK?= =?us-ascii?q?Jc4xqghIOHoUWAwKECD8YAQEBAQEBAQEBAQESAQEBCAsLCCgkC4IzDIMDFQgBF?= =?us-ascii?q?AceAxIQDwIfBwIlEQEFASINCAEBF4l7AQMIDQQMni2DRT+MCoIEBQEcgwkFg1Y?= =?us-ascii?q?KGScNVoMzAQEIAgEdAgYJAQh5gh2DBoIoK4gJgnqCYQWJb41yiA6BaIVnjFhug?= =?us-ascii?q?weHLRGHCpQqM4EVH4FCd3iFDCWBUHSKLwEBAQ?= X-IronPort-AV: E=Sophos;i="5.41,304,1498514400"; d="scan'208";a="233294414" Received: from mail-wm0-f46.google.com ([74.125.82.46]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 31 Jul 2017 18:37:59 +0200 Received: by mail-wm0-f46.google.com with SMTP id m85so81055881wma.0 for ; Mon, 31 Jul 2017 09:37:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:message-id:date:user-agent:mime-version :content-transfer-encoding:content-language; bh=kVNUKNg9aFZHfunSJK5g4vhd/5xA7mRBOsGbnwLm/0k=; b=VSlATznL0Fx4zlzsUb/aAdmVllnULHGW5QpG7VvNJws+9Rnspof2TJooPotH1HA2Ya /m1BR8/tMJcIZ33im59Wv116Lky7teq2Kee3n+QKLQMOVlaT/QnCEl1jdOdhgQwP8un0 zCCrehFx6U5DiGNlKSKHRUjGMIcOPS4ZG++dLECXTl/Wb2Y1gWfHY/4ElW3Yx55JSRYH Ac5kRYX7uxxxzj78jr38L+xPIj8g41OPdqgxD7OrMBl/upDXf+nB9Er9FE3/zl91UvTO 1eqIBDit8Gl64Z+/CtAgadX0kbRJ5o1VNArPoi54ebq27+BgJ9V5+XukSjesah/aOz7O tuPQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:subject:to:message-id:date:user-agent :mime-version:content-transfer-encoding:content-language; bh=kVNUKNg9aFZHfunSJK5g4vhd/5xA7mRBOsGbnwLm/0k=; b=BhhcnH9jhKfLysGT5UlbUjnFVu9+RGsgnM66puBGBC4LQh1cZayIPzzHtSEzPOUvWa Nf72q5nWvgvrpWH2f9p0tP/4fkb+YXNVc5oQJNsG3HoA6ujyjyYbnVIB9PQmG4qkDiwp XtL0Bl0AAM3VBwtEBkDPehxGfvdJXNI+ADAfMhEmNJ6XtT709wkg/ZlymKTazCOhBfnf RZP1bGLxRHNS1Zuopc2fmLQzQBx17tIOEWQzV745gmo2F6k5DRsTL519gUv15Edfcbab U53KFTaToSaRM95h1u26YCBY3Uh0tyHYqHv7r9ELWImBu4Nz/lmUrlSCDXbFLzZeGTIw O0Mg== X-Gm-Message-State: AIVw110aMdzSrf7MEy2gLN8pRPqLC5ET6g29igfhvvgP4o87dTqVxzPl mbYCnqHcdXWW7CpR10I= X-Received: by 10.28.208.202 with SMTP id h193mr11113772wmg.101.1501519078621; Mon, 31 Jul 2017 09:37:58 -0700 (PDT) Received: from [192.168.1.62] (197.45.130.77.rev.sfr.net. [77.130.45.197]) by smtp.gmail.com with ESMTPSA id n7sm47175208wrb.37.2017.07.31.09.37.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 31 Jul 2017 09:37:58 -0700 (PDT) From: Mohamed Iguernlala To: "caml-list@inria.fr" Message-ID: <05deee1e-ef15-daa7-80df-16e214bb9ea3@gmail.com> Date: Mon, 31 Jul 2017 18:37:57 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US Subject: [Caml-list] Loading of dynamic code works with older OCaml versions, but fails with recent versions (>= 4.02.0) Hello, I'm facing an issue[1] with OCaml versions >= 4.02.0 when building/using dynamically loaded plugins for/with Alt-Ergo. I think this is probably due to module aliases. In fact, I'm able to install and use Alt-Ergo + satML-plugin on OCaml 4.01.0, but not on OCaml 4.02.0 (or higher). $ opam sw 4.01.0 $ eval `opam config env` $ opam remove alt-ergo satML-plugin $ opam install alt-ergo satML-plugin $ echo "goal g: 1 + 1 = 2" > foo.why $ alt-ergo -sat-plugin satML-plugin.cmxs foo.why File "foo.why", line 1, characters 9-18:Valid (0.0000) (0 steps) $ opam sw 4.02.0 $ eval `opam config env` $ opam remove alt-ergo satML-plugin $ opam install alt-ergo satML-plugin $ echo "goal g: 1 + 1 = 2" > foo.why $ alt-ergo -sat-plugin satML-plugin.cmxs foo.why ... >> Failure message: implementation mismatch on Options Is this a known issue (or is it an issue) ? I know that if I build the binary and the plugin from the same compiled files, things work well. I was wondering if there is a better solution that allows to build things separately. Regards, Mohamed. [1] https://github.com/OCamlPro/alt-ergo/issues/22 -- Mohamed IGUERNLALA Senior R&D Engineer, OCamlPro SAS Research Associate, VALS team, LRI Webpage: http://www.iguer.xyz LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979