From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:403:4789::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms9.migadu.com with LMTPS id YAKtNneXvmQAZAAASxT56A (envelope-from ) for ; Mon, 24 Jul 2023 17:23:35 +0200 Received: from aspmx1.migadu.com ([2001:41d0:403:4789::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id SHbENneXvmRo0gAA9RJhRA (envelope-from ) for ; Mon, 24 Jul 2023 17:23:35 +0200 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 845903ABE8 for ; Mon, 24 Jul 2023 17:23:35 +0200 (CEST) Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=Ryn2n4c0; spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none) ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1690212215; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=zLlao+TaonkdAXJnIabhv8upXrHPc+HI+kyzn7WUE+0=; b=FjbMDE9cyW2eLS5pkWUDqkmlJZh/rexf9t1eNGqKx/LYAGpnSjp8K0xVAP80vOoiGEJIbg XGDqkP2JWuMSutKg7dafbwzgKzHA5SIAO7Oa1DZcyx/DKATywK8nS3o1Vb1en9yYLXZqbh gyBKHTqgSgA7TF4Lvq/Oqdd58Y8ULYpc9jmjQF982baILd0094VL1gLw9WZgyXXG3J/id7 aWk1mvF2wvGatYMm8618QeKM2Ubure7/qYKHOww0vF/ImJstvnxTix3/4KW6Rwdu/Z5JZA MoK4fdnX56b2Cj85aYz9r4tx8Rmjz5nxYfRH7qFcBd6GWe9SFPdAxZEor7S2MQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1690212215; a=rsa-sha256; cv=none; b=vAOF7Tliw7HsAnwvcZM1iAKvxBYSH85Y5peZSHzKByEKvl5ie+RIGhs1qXip8gnChpeQ1i 6aZ0r+lMeIdeVM5/O+++jmlSZ8+06pCkZ1yHR3joy7QqCXdSqRhKgiEgYfDlxlIAIaQa7a PqQtCH0xSBR7oY+ijZ7XYU8vs0EFskcrRzg5NejyQ2p2gOcqWaL+o4FmFaAIu+i1t5PDNF Ei9/ZApYcUI7/SdpDVcIyndnjc3VrAlQ/ZAvzl62WhON04YNqd2tA6Sk5boGxknrwpHceu 2khod1kUwPhIKxJZVihIgkkRegkfuY4SiU3ve3C2DgrBFgn/kqhfSdKIwXhKyQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=Ryn2n4c0; spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1qNxOy-00018p-Tk; Mon, 24 Jul 2023 11:23:13 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qNxOp-00018M-PC for guix-patches@gnu.org; Mon, 24 Jul 2023 11:23:04 -0400 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qNxOo-0001Fc-Hk for guix-patches@gnu.org; Mon, 24 Jul 2023 11:23:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1qNxOo-0002ns-3h for guix-patches@gnu.org; Mon, 24 Jul 2023 11:23:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#64249] [PATCH ocaml-team v3 2/6] gnu: coq: Update to 8.17.1. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 24 Jul 2023 15:23:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 64249 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: pukkamustard Cc: DABY-SEESARAM Arnaud , 64249@debbugs.gnu.org, Josselin Poiret Received: via spool by 64249-submit@debbugs.gnu.org id=B64249.169021214810732 (code B ref 64249); Mon, 24 Jul 2023 15:23:02 +0000 Received: (at 64249) by debbugs.gnu.org; 24 Jul 2023 15:22:28 +0000 Received: from localhost ([127.0.0.1]:43799 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qNxOF-0002n2-CP for submit@debbugs.gnu.org; Mon, 24 Jul 2023 11:22:27 -0400 Received: from lepiller.eu ([2a00:5884:8208::1]:49504) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qNxOC-0002mm-7V for 64249@debbugs.gnu.org; Mon, 24 Jul 2023 11:22:26 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 261af57a; Mon, 24 Jul 2023 15:22:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:in-reply-to:references:message-id:mime-version :content-type:content-transfer-encoding; s=dkim; bh=/fLOl++g9cn1 /h9gBvSdt9xq6ev1cKRA/bZAcUhtCnY=; b=Ryn2n4c0urGStDEDiQLxv2PZm8J2 W5W5zgT2IcVEb6Ev8QDLDdnORLHLB7NEhC6LzqPSS/A2/D15UMEpBgfgHkuyosKX N6fIIR415Z7aoinKSL6bSt/FLxxvW3gyxSEIPt3Znx8IcJD14SyH7Jtd4+ZoQo59 /0NbZwQn2vdumFgycPiNJKN0toRjXZFbXtUYNwxI8vXSNAJCJajC9soXdnfLoEvK z7THYhFqB02nbEoLL1Q9j5tFaY3j0sM3zV8rb3CZPjzm76hLQMtjaujZQWDsVVpq y5mRo/YC5JWSW3+VWiSI91oDx9fIpdNjD4Egr1wP56UP7vBLtWpLKCmeEQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id ab35c659 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:NO); Mon, 24 Jul 2023 15:22:19 +0000 (UTC) Date: Mon, 24 Jul 2023 17:22:14 +0200 From: Julien Lepiller User-Agent: K-9 Mail for Android In-Reply-To: <86sf9dny39.fsf@posteo.net> References: <858ebb8d740c7bfd0d55eaaf8a67db2298d4081a.1689682321.git.pukkamustard@posteo.net> <20230719201843.31b30208@lepiller.eu> <86sf9dny39.fsf@posteo.net> Message-ID: <7F0D4C89-4838-4C95-82FA-42A49E4119A9@lepiller.eu> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: guix-patches-bounces+larch=yhetil.org@gnu.org X-Migadu-Country: US X-Migadu-Flow: FLOW_IN X-Migadu-Spam-Score: -3.55 X-Spam-Score: -3.55 X-Migadu-Queue-Id: 845903ABE8 X-Migadu-Scanner: mx1.migadu.com X-TUID: R4aR2AjbPi8M I don't see how one would use coq-core without coq-stdlib and coq-stdlib de= pends on coq-core, so I think it's fine to merge these packages=2E It might= make the package definition a bit harder, since there isn't a single dune = target, but I'm fine with it=2E Le 24 juillet 2023 16:54:05 GMT+02:00, pukkamustard a =C3=A9crit=C2=A0: > >Hi, > >Julien Lepiller writes: > >> I'm not sure why, but this is breaking all coq dependents, with >> messages similar to: >> >> cannot guess a path for Coq libraries; please use -coqlib option or >> ensure you have installed the package containing Coq's stdlib >> (coq-stdlib in OPAM) If you intend to use Coq without a standard >> library, the -boot -noinit options must be used=2E >> >> I think this is because coq-stdlib is mostly empty for some reason=2E > >A couple of build failures later this is where I'm at: > >- Coq 8=2E17=2E1 includes considerable changes to the build system=2E > >- Some `dune` files are autogenerated with `make dunestrap` (which runs > the OCaml program `tools/dune_rule_gen/gen_rules=2Eml`=2E > >- In the v3 patches I submitted `make dunestrap` was not being run, > resulting in missing dune files and a quite empty `coq-stdlib` > package=2E > >- The 8=2E17=2E1 generated dune files for `coq-stdlib` reference things i= n > `coq-core` directly with relative paths instead of letting > dune/findlib find them (with entries in the `libraries` stanza in dune > files)=2E This makes building `coq-core` and `coq-stdlib` seperately > more tricky=2E > >I've asked in #coq for ideas on how `coq-stdlib` and `coq-core` can be >built seperately/kept in separate packages=2E Nothing yet=2E > >What do you think about merging `coq-core`, `coq-stdlib` and `coq` into >a single package? Not as nice as the current situation, but maybe a way >to go without too many custom patches/hacks? > >CC: Arnaud and Josselin who might be interested in Coq stuff=2E > >Thanks, >pukkamustard > > >>> * gnu/packages/coq=2Escm (coq-core, coq-stdlib, coq): Update to 8=2E17= =2E1 >>> and remove test-target argument=2E >>> --- >>> gnu/packages/coq=2Escm | 24 +++++------------------- >>> 1 file changed, 5 insertions(+), 19 deletions(-) >>>=20 >>> diff --git a/gnu/packages/coq=2Escm b/gnu/packages/coq=2Escm >>> index 09ca4030ea=2E=2E3332707a71 100644 >>> --- a/gnu/packages/coq=2Escm >>> +++ b/gnu/packages/coq=2Escm >>> @@ -53,7 +53,7 @@ (define-module (gnu packages coq) >>> (define-public coq-core >>> (package >>> (name "coq-core") >>> - (version "8=2E16=2E1") >>> + (version "8=2E17=2E1") >>> (source >>> (origin >>> (method git-fetch) >>> @@ -63,7 +63,7 @@ (define-public coq-core >>> (file-name (git-file-name name version)) >>> (sha256 >>> (base32 >>> - "0ljpqhh5lfsim29fcfp2xfcvm3j84pf1mb0gnpdr8vcqqw7mqwpf")) >>> + "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63")) >>> (patches (search-patches "coq-fix-envvars=2Epatch")))) >>> (native-search-paths >>> (list (search-path-specification >>> @@ -83,8 +83,7 @@ (define-public coq-core >>> (native-inputs >>> (list ocaml-ounit2 which)) >>> (arguments >>> - `(#:package "coq-core" >>> - #:test-target "=2E")) >>> + `(#:package "coq-core")) >>> (properties '((upstream-name =2E "coq"))) ; also for inherited >>> packages (home-page "https://coq=2Einria=2Efr") >>> (synopsis "Proof assistant for higher-order logic") >>> @@ -101,19 +100,7 @@ (define-public coq-stdlib >>> (inherit coq-core) >>> (name "coq-stdlib") >>> (arguments >>> - `(#:package "coq-stdlib" >>> - #:test-target "=2E" >>> - #:phases >>> - (modify-phases %standard-phases >>> - (add-before 'build 'fix-dune >>> - (lambda _ >>> - (substitute* "user-contrib/Ltac2/dune" >>> - (("coq-core=2Eplugins=2Eltac2") >>> - (string-join >>> - (map (lambda (plugin) (string-append >>> "coq-core=2Eplugins=2E" plugin)) >>> - '("ltac2" "number_string_notation" "tauto" >>> "cc" >>> - "firstorder")) >>> - " ")))))))) >>> + `(#:package "coq-stdlib")) >>> (inputs >>> (list coq-core gmp ocaml-zarith)) >>> (native-inputs '()))) >>> @@ -123,8 +110,7 @@ (define-public coq >>> (inherit coq-core) >>> (name "coq") >>> (arguments >>> - `(#:package "coq" >>> - #:test-target "=2E")) >>> + `(#:package "coq")) >>> (propagated-inputs >>> (list coq-core coq-stdlib)) >>> (native-inputs '()))) >