From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0.migadu.com ([2001:41d0:303:e224::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms1.migadu.com with LMTPS id eOE/B6J4KmbGrwAAqHPOHw:P1 (envelope-from ) for ; Thu, 25 Apr 2024 17:37:06 +0200 Received: from aspmx1.migadu.com ([2001:41d0:303:e224::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0.migadu.com with LMTPS id eOE/B6J4KmbGrwAAqHPOHw (envelope-from ) for ; Thu, 25 Apr 2024 17:37:06 +0200 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=none; 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=none ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1714059425; 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: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; bh=R+JN5X3wz00kdKczA/QakxHJ/hSQU2QCHJ7wEupI808=; b=dvGGiXcZZiqek+5eRQB8ZBdtF4rW7J51470R9PmnVWPePV4W7WUoH+lekGFbH3mBNpZKWW OBmmhhH8JqYe3tTVxn5be4histCW0J05pfhS65yCdWcvx2rx0MUN5c+ac8mdq2L4LnjCGy +OIvizCP7dSbrVAtqfYuTJDlbuIfNBcyrWlUqrq9rbxfWh4+Hc+1l+pTt02/n9g9lpwYP1 rHI+SKwjHw0XlohaoxQBJ2INgSRmakJXid4FOZrqE3sTMg3zcy9JLo2jQoiQaOQhisU3PB fMp5oXLNByYIJ2WvaDNH18hS8MBD+3ZavDvcOZO0K8rrEPUMc3KEHVDR8/Gyfw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1714059425; a=rsa-sha256; cv=none; b=FF2vEBABAJQe5wKk6DK0bsjN30tB0Z/mg47Wv9lKFu3MTOURM6XWx7vR4p3lMSlP/eDpa7 O6DTwkBX4EYKR19DxKJbFjZZeBFY7NBr8BlyOazi8WxB8hcbTEivuCgQEcw2XhD2mV4Nna sWRO1SPOmRthJkCUX6IKF+qrmR6c9pdNLwvhYYYfWUhuTG9OCqHhCN/nQEuzHMIwDnqrXQ CZor8aNo6aKGVtcOdDstnH1S9nPFvtYNPZPqHaSU0uCI3DPh6adiNVTYoOKetQYOLkODkY +qquD0jNR3kxRDoelMGWRuT94wmPFJj3eEL0tjFbb1ET18JCqm9wH5g1hzRjkg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=none; 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=none 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 C9E9A32E9A for ; Thu, 25 Apr 2024 17:37:05 +0200 (CEST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1s019g-0001Nr-K3; Thu, 25 Apr 2024 11:37:00 -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 1s019Y-0001KZ-DY for guix-patches@gnu.org; Thu, 25 Apr 2024 11:36:53 -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 1s019Y-00031Y-4x for guix-patches@gnu.org; Thu, 25 Apr 2024 11:36:52 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1s019p-0003Hh-Np for guix-patches@gnu.org; Thu, 25 Apr 2024 11:37:09 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#70567] [PATCH 0/7] frama-c: Update to 28.1. Resent-From: Andreas Enge Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 25 Apr 2024 15:37:09 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 70567 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Julien Lepiller Cc: 70567@debbugs.gnu.org, Arnaud Daby-Seesaram , Sharlatan Hellseher , Jean-Pierre De Jesus DIAZ , Eric Bavier Received: via spool by 70567-submit@debbugs.gnu.org id=B70567.171405937612028 (code B ref 70567); Thu, 25 Apr 2024 15:37:09 +0000 Received: (at 70567) by debbugs.gnu.org; 25 Apr 2024 15:36:16 +0000 Received: from localhost ([127.0.0.1]:33031 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1s018w-00037g-Px for submit@debbugs.gnu.org; Thu, 25 Apr 2024 11:36:15 -0400 Received: from hera.aquilenet.fr ([2a0c:e300::1]:53310) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1s018p-00035V-VV for 70567@debbugs.gnu.org; Thu, 25 Apr 2024 11:36:09 -0400 Received: from localhost (localhost [127.0.0.1]) by hera.aquilenet.fr (Postfix) with ESMTP id 44ED7CD3; Thu, 25 Apr 2024 17:35:43 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at hera.aquilenet.fr Received: from hera.aquilenet.fr ([127.0.0.1]) by localhost (hera.aquilenet.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id IghpAksSdhSi; Thu, 25 Apr 2024 17:35:42 +0200 (CEST) Received: from jurong (unknown [IPv6:2001:861:c4:f2f0::c64]) by hera.aquilenet.fr (Postfix) with ESMTPSA id 89819CB8; Thu, 25 Apr 2024 17:35:42 +0200 (CEST) Date: Thu, 25 Apr 2024 17:35:41 +0200 From: Andreas Enge Message-ID: References: <8734r9a3x1.fsf@nanein.fr> <23FB3A3D-8FED-418D-AF36-0EF59C95F0E7@lepiller.eu> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <23FB3A3D-8FED-418D-AF36-0EF59C95F0E7@lepiller.eu> 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-Flow: FLOW_IN X-Migadu-Country: US X-Migadu-Spam-Score: -4.99 X-Spam-Score: -4.99 X-Migadu-Queue-Id: C9E9A32E9A X-Migadu-Scanner: mx12.migadu.com X-TUID: F8GX9ugh2ebe Hello, looking at what frama-c does, I am a bit puzzled: to me it has been put into the wrong module, together with why3 just above it; unless you consider informatics as a subset of mathematics, that is. In any case, these packages do not seem to do computations of interest to an applied mathematician (which is what most of maths.scm is about) or a pure mathematician (with packages in algebra.scm). Could they be moved to coq.scm? Or a more generic, maybe a new module related to theorem proving and/or source code analysis? Maybe into a renamed valgrind.scm? Andreas