From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id +F5hH2a9PWMBQAAAbAwnHQ (envelope-from ) for ; Wed, 05 Oct 2022 19:22:46 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id oCp6H2a9PWMEgAAA9RJhRA (envelope-from ) for ; Wed, 05 Oct 2022 19:22:46 +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 01E22223EA for ; Wed, 5 Oct 2022 19:22:46 +0200 (CEST) Received: from localhost ([::1]:35420 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1og86X-0008QJ-6C for larch@yhetil.org; Wed, 05 Oct 2022 13:22:45 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:52440) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1og85r-0007Wb-2H for guix-patches@gnu.org; Wed, 05 Oct 2022 13:22:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:58864) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1og85q-00005J-P7 for guix-patches@gnu.org; Wed, 05 Oct 2022 13:22:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1og85q-0006P3-BD for guix-patches@gnu.org; Wed, 05 Oct 2022 13:22:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#58310] [PATCH] Add coq-mathcomp-analysis Resent-From: Garek Dyszel Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Wed, 05 Oct 2022 17:22:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 58310 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 58310@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.166499048624567 (code B ref -1); Wed, 05 Oct 2022 17:22:02 +0000 Received: (at submit) by debbugs.gnu.org; 5 Oct 2022 17:21:26 +0000 Received: from localhost ([127.0.0.1]:57942 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1og85G-0006OA-Hl for submit@debbugs.gnu.org; Wed, 05 Oct 2022 13:21:26 -0400 Received: from lists.gnu.org ([209.51.188.17]:42590) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1og85C-0006O1-Ew for submit@debbugs.gnu.org; Wed, 05 Oct 2022 13:21:24 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:44320) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1og85C-0006kR-8X for guix-patches@gnu.org; Wed, 05 Oct 2022 13:21:22 -0400 Received: from knopi.disroot.org ([178.21.23.139]:38082) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1og859-0008Nx-IM for guix-patches@gnu.org; Wed, 05 Oct 2022 13:21:21 -0400 Received: from localhost (localhost [127.0.0.1]) by disroot.org (Postfix) with ESMTP id EF27B4C708 for ; Wed, 5 Oct 2022 19:21:14 +0200 (CEST) X-Virus-Scanned: SPAM Filter at disroot.org Received: from knopi.disroot.org ([127.0.0.1]) by localhost (disroot.org [127.0.0.1]) (amavisd-new, port 10024) with UTF8SMTP id dGT29zmG0Mwv for ; Wed, 5 Oct 2022 19:21:13 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=disroot.org; s=mail; t=1664990157; bh=YAXBxKd5J/ygSaiD/vFGKwrJ/bO5tz5zQO4A204r8ZU=; h=From:To:Subject:Date; b=ZEsZ3xDjHxyC7C0rp+rrDWYk5fO73hlHySRy8pgGke9SfXfEXzb8ngoumeXTV1ZfC MWDQ9Ci8zO2OsW75wCQcboXLeuQmzXF3nMM7CZwNi7uV3mbIqg3CG0ON1xXtjtte+8 +zQv0bs95sZlx9WRJr+w6OMliYbFjBys8erJxZ9Tl7MknC6Fs8QkgKJowBLKIirHo8 RJ4qPz94QILGHBQjEQOEUJiFtXgZpZnd4MSAqUcbFm9g6LQe9Nq/V88G/ONWAx7Gqz POJQPcF/BYE3DTojkDjCyvK3rgV9isyja0XsAL8ocPRojBqEtpT/kKInEv8Ci8l5Ju SihsoPvixYW5w== Date: Wed, 05 Oct 2022 13:15:49 -0400 Message-ID: <87h70iqji2.fsf@disroot.org> Mime-Version: 1.0 Content-Type: text/plain Received-SPF: pass client-ip=178.21.23.139; envelope-from=garekdyszel@disroot.org; helo=knopi.disroot.org X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action 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" Reply-to: Garek Dyszel X-ACL-Warn: , Garek Dyszel via Guix-patches From: Garek Dyszel via Guix-patches via X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1664990566; h=from:from:sender:sender:reply-to:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:list-id:list-help:list-unsubscribe:list-subscribe: list-post:dkim-signature; bh=YAXBxKd5J/ygSaiD/vFGKwrJ/bO5tz5zQO4A204r8ZU=; b=CO/ghue4ZyzxYg1Zq0zr9KvJrLA1zsLlD/GTm/VTAMUtUFnWfiR1XBz6Nl0EI5LQJRT07h VQb0HnL6VAforRtbUuRSDwx4/+u3y3femZzz6btVDs6CaJqzYIs8cfIBcFm+zEeOAW9bVp LTaK/8ILblSxL8EEP5/YBCKXdm8iDjgHzDw5nH0jTiuLDUTHzJMqb7AmIp5DifS5Lw7ZHK 4Bs/Hj9v4Cl5WQiEBAqWWJZyhi+9pqVYo2pK20x5HlBRpncdNTD/HeIocNkdKi1zFVSwHf UDJZnZgn4cNKEImKtX8rB+NzS4x7UptqdoFzizcgAdo555AD1liXDaQ5ILKW2g== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1664990566; a=rsa-sha256; cv=none; b=EA/ky719liGZPXcni6Vhsk/+TVK29HC+WVCNUA4mVQtzYb3b3M4BAcos+JuGB9AvAarIrg DwW7W3AF3aRPBoog0KNDm+xObgr4Q+FhTEEpYsMl3Nqg3FzQ/tWHl0ZZZ4ZTsOGDGEKII4 V9lPXlClWT6xBOof3a3zXuIQDTDM5chVSzHdnColQ1S4mHZjN0WjJp5PejiQC9Ur3z0Iz4 UW//BsuMyzQ7RSooG+CrndI0TFIFFctjhZgTzN9KLxg9jg4jiw3ipcJMYDU5zYhTEaWbFk haW5wpVWL690wiQzCFwn/6rjnl5woAarN+xCJD4MXU9eJ6DIqIFpj6frThaKlA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=disroot.org header.s=mail header.b=ZEsZ3xDj; dmarc=pass (policy=none) header.from=gnu.org; 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" X-Migadu-Spam-Score: -3.36 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=disroot.org header.s=mail header.b=ZEsZ3xDj; dmarc=pass (policy=none) header.from=gnu.org; 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" X-Migadu-Queue-Id: 01E22223EA X-Spam-Score: -3.36 X-Migadu-Scanner: scn0.migadu.com X-TUID: XChvPJ/yo0/S This patch set adds coq-mathcomp-analysis, but it does not build correctly. The build process for ocaml-elpi@1.16.5 is broken. I did, however, get coq-mathcomp-analysis to successfully build when using an older version: ocaml-elpi@1.15.2, which builds just fine. To aid in debugging, I left the information for both versions of ocaml-elpi in the commit which adds ocaml-elpi (ocaml-elpi@1.15.2's info is commented out). We will have to see whether it's possible to upgrade coq-elpi to 1.15.6 without breaking coq-mathcomp-hierarchy-builder. The same goes for whether it's possible to upgrade coq-mathcomp-hierarchy-builder to 1.4.0 without breaking coq-mathcomp-analysis. There is an unresolved warning from guix lint that says "python-hatch@1.5.0: can be upgraded to 1.10.0". In fact, both python-hatch and python-hatch-bootstrap are located in the same repository, and the newest tag for hatch is hatch-v1.5.0. In this case, guix lint is incorrect. Let me know what you think!