Huỳnh Trần Khanh (Jul 25 2022 at 14:36): Huỳnh Trần Khanh (Jul 25 2022 at 14:36):I used to be a Lean user, now I want to switch to Coq. After going through some Software Foundations exercises, I found that Coq is somewhat similar to Lean. Coq runs blazingly fast even on the web. I am a competitive programmer and I want to use Coq for training purposes and also to explain solutions to problems! So, to learn the basics there is the helpful Software Foundations tutorial. As an ex Lean user, are there things that I need to unlearn in order to use Coq?
Huỳnh Trần Khanh (Jul 25 2022 at 14:37):A long long time ago I already asked for a comparison between various systems. Your answers are very helpful.
Karl Palmskog (Jul 25 2022 at 14:42):@Huỳnh Trần Khanh there is unfortunately no canonical comparison between Coq and Lean. There are many features that are unique to each system individually. I can at least recommend https://github.com/coq-community/awesome-coq which lists many resources and libraries and plugins for Coq. In comparison to Lean, where Mathlib is the central library, Coq has many different libraries to choose from.
We compare some high-level aspects of Coq and Lean here: https://hal.inria.fr/hal-03592675v2/document#page=10
Karl Palmskog (Jul 25 2022 at 14:48):for a comparison of foundational differences, there is the classic: https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581
Huỳnh Trần Khanh (Jul 25 2022 at 14:50):Thanks to the cross-platform binary format for compiled code used by Lean,
mathlib can be easily distributed both in source and binary form, which generally
leads to a faster setup than for comparable Coq libraries which are compiled from
source.
Color me confused. Coq also has object files right? Can't I just download some object files from some CI to speed things up?
Huỳnh Trần Khanh (Jul 25 2022 at 14:52):we believe the operating-system-specific binary distributions of the Platform have comparable ease of use.
I can't read sorry :neutral: So the object files are just platform specific, but I can still download them off of somewhere. Is this correct?
Huỳnh Trần Khanh (Jul 25 2022 at 14:55):I might need a detailed explanation about how these files work. I did a quick search and found that Coq does things quite differently.
Karl Palmskog (Jul 25 2022 at 15:00):Coq has object files like .vo, but they don't work across Coq versions
Karl Palmskog (Jul 25 2022 at 15:01):and also, they don't work across different versions of the OCaml compiler (which compiled Coq). This typically means .vo files are not portable across Linux/Mac/Windows
Karl Palmskog (Jul 25 2022 at 15:02):however, most people rely on the opam package manager to install Coq-related things, including Coq libraries and plugins, and opam is based on source code, so the binary file problem doesn't pop up too often
Karl Palmskog (Jul 25 2022 at 15:04):we recommend beginners to use the Coq Platform to install Coq, it has both source-based opam installation and binary packages for download
Huỳnh Trần Khanh (Jul 26 2022 at 14:29):Are there any competitive programmers using Coq? I'd like to see competitive programming related projects in Coq.
Huỳnh Trần Khanh (Jul 26 2022 at 14:29):For example, I'd love to see a formalized Fenwick tree.
Lessness (Jul 26 2022 at 15:00):I have first two Project Euler exercises formalized... :sweat_smile: Not exactly programming competition stuff, though. :sweat_smile:
(Written in C and then proven correct using VST. See here how it looks: https://github.com/LessnessRandomness/PE)
What exactly do you mean by formalizing Fenwick tree?
Huỳnh Trần Khanh (Jul 26 2022 at 15:15):A Fenwick tree is a data structure that helps you calculate range sum quickly. Project Euler is pretty close to competitive programming, some competitive programmers also solve problems there too. I guess your repository counts!
Huỳnh Trần Khanh (Jul 26 2022 at 15:16):So, formalizing a Fenwick tree means proving that a piece of code that uses Fenwick tree to answer range sum queries works correctly.
Huỳnh Trần Khanh (Jul 26 2022 at 15:16):If you are inclined, I encourage you to try out competitive programming. It's fun.
Huỳnh Trần Khanh (Jul 26 2022 at 15:24):I really want to use VST but the licenses discouraged me from trying it out. It's not really free software and I can easily get into trouble for using it. I'm researching alternatives.
Lessness (Jul 26 2022 at 15:29):Yeah, I sent an email to Absint a week ago (they sell licences for clightgen.exe tool and also Compcert compiler).
If I want to use clightgen.exe tool commercially, I have to pay €5980.50 for the licence. If I wanted to use Compcert compiler, it would cost me even more, I believe.
Lessness (Jul 26 2022 at 15:32):Which isn't that much actually, given the work it took to make all these tools. I would pay them if I had the money, gladly. But I'm poor student. :sweat_smile:
Karl Palmskog (Jul 26 2022 at 15:35):did you guys see the Kata stuff? https://www.codewars.com/kata/search/coq
Karl Palmskog (Jul 26 2022 at 15:39):Huỳnh Trần Khanh said:
I really want to use VST but the licenses discouraged me from trying it out. It's not really free software and I can easily get into trouble for using it. I'm researching alternatives.
@Huỳnh Trần Khanh did you see the VST and CompCert license discussion here? I think it's pretty clear that VST itself is open source, but sure, if you want to convert real C code to Clight, clightgen proprietary license stands in the way.
Karl Palmskog (Jul 26 2022 at 15:49):probably some nice challenges left here in converting https://functional-algorithms-verified.org to Coq/SSReflect/MathComp: https://github.com/clayrat/fav-ssr
Last updated: Oct 01 2023 at 17:01 UTC