From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 13F1F5D6 for ; Mon, 11 Oct 2021 21:27:52 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.84,326,1620684000"; d="scan'208,217";a="533331804" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 11 Oct 2021 23:27:50 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 2763AE019E; Mon, 11 Oct 2021 23:27:50 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 3E70EE003C for ; Mon, 11 Oct 2021 23:27:46 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mjp.pereira@fct.unl.pt; spf=Pass smtp.mailfrom=mjp.pereira@fct.unl.pt; spf=None smtp.helo=postmaster@mail-io1-f49.google.com IronPort-PHdr: =?us-ascii?q?A9a23=3ACEpe7h2fZxdgfMCcsmDOZAQyDhhOgF0UFjAc5pd?= =?us-ascii?q?vsb9SaKPrp82kYBaHo6Q0xwKWFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkel?= =?us-ascii?q?M8NlBYhCsPWQWfyLfrtcjBoVJ8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZ?= =?us-ascii?q?pO+j5AIHfg9qr2+yo/5DffgpEiTq/bLhvMBi4sALdu9UMj4B/MKgx0BzJonVJe?= =?us-ascii?q?+RS22xlIE+Ykgj/6Mmt4pNt6jxctP09+cFOV6X6ZLk4QqdDDDs6KWA15dbkugf?= =?us-ascii?q?FQACS+3YTSGQWkh5PAwjY8BH3W4r6vyXmuuZh3iSRIMv7Rq02Vzu/9admUBDni?= =?us-ascii?q?CkFODA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoS?= =?us-ascii?q?yYJEVD+oAOuZTspPzqEUUrRSgBAmsHvngwSJPi3/z3606y/4tERnY0ww6Ad0Os?= =?us-ascii?q?W7Uo8/uOaccTe+10LPEzSjFb/NSwzv98JTIfwknrPqRUr1+bdDfxlMzFwPZkFq?= =?us-ascii?q?Qs4rlMiuX2+gTs2WW4ORtWOKzhmAnqgx9viWiy8MxhoTNiI8bxF/K+Cp4zYsoK?= =?us-ascii?q?9C1RlN3b9CrHpZSqy2XN4R7Tt48Tmxrvisx17MIuZm+fCcQyZQnwQbSa/OGc4i?= =?us-ascii?q?U4hLjSf2eLS1ki3JifbKznwqy8Umlyu3nUcm0ykpKojBAktnIsH0Gyh/d6tCfR?= =?us-ascii?q?/dj4kus3SyD2gPT5+1ePEw5lKvWJ4Quz7M0kJcYrF7NETXsmErsia+bbkUk9fa?= =?us-ascii?q?s6+Tgerjmo4WTN45wig3nM6QundGzDf02MgUBW2WX4+u81Lrk/U32RLVFkOc6n?= =?us-ascii?q?bXesJDfPcgbp6i5DBFJ0os79RqzEzOr3M4bkHQHNl5JZROKgonzN1zBJP30FfK?= =?us-ascii?q?/jE6tkDdvyfDGJLrhApDVI3jGkrfhZaxx61ZCxwop099f5ohUBasaLfL9RkDxq?= =?us-ascii?q?MbUDgI/Mwyw2ernEMl92psEWW2TGq+ZLL/SsViQ6+0zOeaMYYsVtC/5K/gk/P7?= =?us-ascii?q?ukWQ0mUQdfKmsxZsYcmq0HvVgI0WDYHrjmM0NEWkQvll2cOu/rlyFVSUbM3CzW?= =?us-ascii?q?KYnzjc6D4a9S4nZENODmruEiQKyBJxRLlhLEF2NC36gI4CGQ7EUZTifI9VoujI?= =?us-ascii?q?PSf68TYtnzQ3451yy8KZuMueBon5QjpnkztUgv4U7cDk8/iAyEsKZlXmRHTkcd?= =?us-ascii?q?oIgQjY32OV+phU4xAvSl6d/hPNcGJpY4PYbCm/S2rbSxPA8Ftb2HBrdLI7hdQ?= =?us-ascii?q?=3D=3D?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3AdDQiK6zdrHewXbIYUD3EKrPwIb1zdoMgy1kn?= =?us-ascii?q?xilNoNJuEvBw8Pre/8jztCWftN9/YhAdcLy7V5VoBEmzyXcK2/hyAV7SZmTbUQ?= =?us-ascii?q?KTRekI0WKh+UyEJ8SUzIJgPMlbAsxD4aXLfD9Hsfo=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BEAgCYahphfzGmVdFahgRWOzGER4Eej?= =?us-ascii?q?iuXX4gsCwEDAQ03CgQBAYRhAoJrAh0HAQQ0EwECBBUBAQUBAQECAQMDBAETAQE?= =?us-ascii?q?NCxAIOCaFaA2CNSKDbAIBAxIRHQEBNwEPCwQHNwICIhIBBQEcBjWCUIMHD5p5g?= =?us-ascii?q?QQ9izKBMRNuggcBAQaGKIFaAwYSgSiHCwEBhmYngimBS4JvPoJLFwKCDYJqgmS?= =?us-ascii?q?FUoFevksHgyuKPYZ6jRsrpnWiT5h3ECOBVIF9MxpzMQaCMlAZDpIShWGEfkMvO?= =?us-ascii?q?AIGAQoBAQMJiXUBAQ?= X-IPAS-Result: =?us-ascii?q?A0BEAgCYahphfzGmVdFahgRWOzGER4EejiuXX4gsCwEDAQ0?= =?us-ascii?q?3CgQBAYRhAoJrAh0HAQQ0EwECBBUBAQUBAQECAQMDBAETAQENCxAIOCaFaA2CN?= =?us-ascii?q?SKDbAIBAxIRHQEBNwEPCwQHNwICIhIBBQEcBjWCUIMHD5p5gQQ9izKBMRNuggc?= =?us-ascii?q?BAQaGKIFaAwYSgSiHCwEBhmYngimBS4JvPoJLFwKCDYJqgmSFUoFevksHgyuKP?= =?us-ascii?q?YZ6jRsrpnWiT5h3ECOBVIF9MxpzMQaCMlAZDpIShWGEfkMvOAIGAQoBAQMJiXU?= =?us-ascii?q?BAQ?= X-IronPort-AV: E=Sophos;i="5.84,326,1620684000"; d="scan'208,217";a="533331788" X-MGA-submission: =?us-ascii?q?MDFchtpT/ReTEWCJxbu1NwoEOAk+RsS3ltrNRG?= =?us-ascii?q?UXCSjsgTW2cUANv750ds+OR/bWCgqT3jO1WjaiN/4lxTknFhgmerZ6/u?= =?us-ascii?q?bZOSUSsrd/yxK5Nn0KWeQk247ky3lmSkKAyGMGUZQtHs7CNkI/IpEO6L?= =?us-ascii?q?xpqzmiJNLDurK6ckyQnulgiQ=3D=3D?= Received: from mail-io1-f49.google.com ([209.85.166.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 11 Oct 2021 23:27:44 +0200 Received: by mail-io1-f49.google.com with SMTP id x1so17448115iof.7 for ; Mon, 11 Oct 2021 14:27:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fct.unl.pt; s=googlefct; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=K6K0WQJzZFKQIT2gwBwhX9cRBTeGllosGKz09i02La0=; b=G1XPa20nMGMOllWQI7j41FzlQaVVNOg/aOFbQay9Cc3cvPXPt1opyXU2zZbw7MyL6+ Ma36ZPJ8eOBjG8W1QDxDXo71bnHiuzFz9NOrGldkOU0Rr4ZH6Gd5sGt2T8QQWbzcOIbH +o6DngyQODILY2vJXfdqxI/IEVuWVzWRQgfNd5D1CZTCPH9PPwV/8Tf07s09sZXCuAF/ gvn8vVJpV2klji272VaHkypbiIEZCnFqyr5Xy9Ud/tJAESrVkg6NvT70x3DiF6z281Vg o6mW01Qn8fRZd8IrcsCN8PK8l28bp1cZ3Asvr/8SfMWXfCIYnY69OFtkwFnoHF2+0ND4 +4KA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=K6K0WQJzZFKQIT2gwBwhX9cRBTeGllosGKz09i02La0=; b=IIlccBYO1LMe3l4eCuqUe2y62zq7jNGX6gFk11Px1uxm3bEDzu434Peuq3WIL6ROXy 226TV6Pp6t4wr9h+aBdoxAQE1O63Jdr+m/13W3caMz2rSHaYXjrUBIv3XMPg7LgIax27 5UJg1VjNIJFna9iFfIeoimb/cv3amVLqs5nMYcIeoswbwFruGn5gyx3drl9e+5p10WrM fQ3nAfXVWADcR6dTqL9ws6qxVRgj0m4BjRlqrT+/xPgcmHVKs1wdxT/xb1Qs3laVNQ2V s+Xm9qoLi0ljAu3yTnAK8mUpodTXEqnlh8LIfS9/Sn8XisFmQqa1vzcOuQm37Z2ERN8S xzQg== X-Gm-Message-State: AOAM533XxsDhTe3d6Gh5x8Ng9c+d/TMCEKmFyp1NCQOteHfisPM2JL4P 85uZCyGmgWgNKkKwBRTr/cx/kHwThr527QgSq9IdcyhPsWWIvKfw X-Google-Smtp-Source: ABdhPJxUAlCb2SrAJQ5uo1lYGFyWF4ANOQlPTJzah7E9qD6UkO5LjI14zGwFBlVKj0ZaVHeq14v5W9lkbMb6306BQeY= X-Received: by 2002:a02:aa96:: with SMTP id u22mr7744146jai.95.1633987663052; Mon, 11 Oct 2021 14:27:43 -0700 (PDT) MIME-Version: 1.0 References: <20211009040533.chu7kqqk27r5wcok@oulala> <20211009195910.mqivg4tsafiyb3tr@oulala> <875a3212-c4a1-41fb-65f7-2a68b012af9f@niols.fr> In-Reply-To: <875a3212-c4a1-41fb-65f7-2a68b012af9f@niols.fr> From: Mario Pereira Date: Mon, 11 Oct 2021 22:27:32 +0100 Message-ID: To: Niols Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary="00000000000039555705ce1a6639" Subject: Re: [Caml-list] O(n ln k) sorting for ocaml on github and a challenge Reply-To: Mario Pereira X-Loop: caml-list@inria.fr X-Sequence: 18604 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: --00000000000039555705ce1a6639 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Niols, The repository in question is very experimental. Our implementation of > TimSort on list is indeed broken. I can't remember if it contains the > famous TimSort bug, but we are aware that it exists and know of two ways > to fix it. We quickly switched to working on arrays, though, and were > planning on coming back to list eventually. > > Our implementation of TimSort on arrays can be found here: > > > https://github.com/LesBoloss-es/sorting/blob/master/src/array/timsort.ml > > It does include a fix of the bug. We have tested it successfully on a > rather wide range of arrays. > So interesting that you mentioned this :) I actually came across your implementation as I was looking for an OCaml implementation of TimSort that I could use as a test stress for Cameleer (a deductive verification tool for OCaml-written code). I didn't get that much far (cf, the in-progress proof is here: https://github.com/ocaml-gospel/cameleer/blob/master/examples/in_progress/t= imsort.ml), but I was planning to get back to it very soon. Maybe I will take a look first at the implementation on arrays :) Cheers -- M=C3=A1rio --00000000000039555705ce1a6639 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi=C2=A0Niols,

The = repository in question is very experimental. Our implementation of
TimSort on list is indeed broken. I can't remember if it contains the <= br> famous TimSort bug, but we are aware that it exists and know of two ways to fix it. We quickly switched to working on arrays, though, and were
planning on coming back to list eventually.

Our implementation of TimSort on arrays can be found here:


https://github.com/LesBoloss= -es/sorting/blob/master/src/array/timsort.ml

It does include a fix of the bug. We have tested it successfully on a
rather wide range of arrays.

So interes= ting that you mentioned this :) I actually came across your implementation = as I was looking=C2=A0for an OCaml implementation of TimSort that I could u= se as a test stress for Cameleer (a deductive verification tool for OCaml-w= ritten code).=C2=A0

I didn't get that much= far (cf, the in-progress proof is here:=C2=A0https:/= /github.com/ocaml-gospel/cameleer/blob/master/examples/in_progress/timsort.= ml), but I was planning to get back to it very soon. Maybe I will take = a look first at the implementation on arrays :)

Ch= eers
--
M=C3=A1rio
--00000000000039555705ce1a6639--