Zulip Chat Archive

Stream: lean4

Topic: Submit Lean code on online judges

Huỳnh Trần Khanh (Jul 28 2022 at 15:37):

I do competitive programming. I need to submit Lean 4 code to online judges. Online judges don't support Lean 4 so I have to find a way to wrap Lean 4 in a more common language. For example, if there is an easy way to compile Lean 4 code to WebAssembly, I could just do it and wrap the WebAssembly code in Node.js. Alas, there isn't. The most popular online judge is Codeforces. To view the list of languages Codeforces supports, head over to https://codeforces.com/contest/1281/status and click the "Any language" drop-down box. Could you give me some hacky ideas that I can attempt so I can submit Lean code there?

Codeforces runs on Windows. Other online judges mostly run on Linux.

Arthur Paulino (Jul 28 2022 at 17:23):

If you're feeling motivated, I believe it's possible to generate Haskell code from Lean 4 code via metaprogramming. That is, you create a Lean 4 program that runs Lean.Elab.runFrontend on a Lean 4 source and then you work your way through the environment that's generated

Arthur Paulino (Jul 28 2022 at 17:24):

An Environment is mainly a set of "constants": axioms, theorems, definitions, inductives etc

Arthur Paulino (Jul 28 2022 at 17:53):

This is not too simple though. You want to make sure that your Lean 4 source doesn't make use of things that are implemented externally via FFI so everything you're transpiling is implemented in Lean 4 itself.

Also, the environment contains a lot of things that you won't need. So you better start your transpilation routine from some main function and dig the environment on demand

Mac (Jul 28 2022 at 18:33):

@Huỳnh Trần Khanh I guess you could conceivable submit the compiled C code Lean produces?

Huỳnh Trần Khanh (Jul 29 2022 at 06:12):

Doesn't the generated code depend on a runtime library? I guess we also need to copy and paste the runtime library too as well right?

Huỳnh Trần Khanh (Jul 29 2022 at 06:12):

Also, I can't submit too much code.

Huỳnh Trần Khanh (Jul 29 2022 at 06:18):

Here's a concrete challenge. Solve this problem with Lean. Then tell me how you do it.

Huỳnh Trần Khanh (Jul 29 2022 at 06:26):

If this is not possible, I still have another hack. I'll make my own programming language! And then I'll make a transpiler into Lean and a transpiler into C++. It's not ideal but I have too much free time and I'm willing to do anything to make this stuff work. This is a new frontier after all.

I just want to kiss deep embedding goodbye.

Eric Wieser (Jul 29 2022 at 10:05):

Arthur Paulino said:

If you're feeling motivated, I believe it's possible to generate Haskell code from Lean 4 code via metaprogramming. That is, you create a Lean 4 program that runs Lean.Elab.runFrontend on a Lean 4 source and then you work your way through the environment that's generated

Doesn't that assume that the semantics of (non-tactic) lean code embed faithfully in haskell? A cursory google suggests haskell doesn't really support dependent types

Huỳnh Trần Khanh (Jul 29 2022 at 10:29):

Honestly, if I'm good enough to follow Arthur's approach then I might as well join the Lean development team. It's probably as complex as making a new compilation target. And we know all too well how arduous this work is...

Henrik Böving (Jul 29 2022 at 10:32):

I mean translating to Haskell is a new compilation target :P

Eric Wieser said:

Arthur Paulino said:

If you're feeling motivated, I believe it's possible to generate Haskell code from Lean 4 code via metaprogramming. That is, you create a Lean 4 program that runs Lean.Elab.runFrontend on a Lean 4 source and then you work your way through the environment that's generated

Doesn't that assume that the semantics of (non-tactic) lean code embed faithfully in haskell? A cursory google suggests haskell doesn't really support dependent types

We can already translate Lean code to semantically equivalent C code so I dont see why we shouldn't be able to build Haskell code, just because the original source was Lean doesnt mean the dependent types have to be preserved as the C backend shows

Eric Wieser (Jul 29 2022 at 10:33):

I was reading the suggestion as "it's a straightforward 1:1 mapping", which I'm sure is not really true at all for the C compilation

Eric Wieser (Jul 29 2022 at 10:34):

@Huỳnh Trần Khanh, have you taken a look at the C code output to see how viable using it would be?

Henrik Böving (Jul 29 2022 at 10:36):

The C output is really not nice to the reader, all variable names are replaced with xN where N is some number, constructors are referred to by numbers etc. And it is also quite long so the "too much code" criteria will hit sooner or later I assume.

Henrik Böving (Jul 29 2022 at 10:42):

To demonstrate this is the first few lines of C in the main function:

LEAN_EXPORT lean_object* _lean_main(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = lean_get_stdin(x_1);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_ctor_get(x_3, 4);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_apply_1(x_5, x_4);

for

def main : IO Unit := do
  let stdin ← IO.getStdin
  let inputLine ← stdin.getLine
  let kilos := inputLine.toNat!
  if kilos % 2 == 0 then
    IO.println "Yes"
  else
    IO.println "No"

If you are wondering, the x_1 it is pulling through to getStdin etc. is indeed RealWorld.

Huỳnh Trần Khanh (Jul 29 2022 at 10:49):

Ugh. All the refcount calls, and also there is the runtime library that I need to copy and paste too.

The size of the file with the source code shouldn't exceed 64 kilobytes. https://codeforces.com/blog/entry/4088

Damiano Testa (Jul 29 2022 at 10:51):

Is there a condition that kilos should be at least 4, in the question? In the solution? :upside_down:

Huỳnh Trần Khanh (Jul 29 2022 at 10:51):

Will the massive amount of code prevent us from solving Watermelon? Too bad I still don't have Lean 4 installed on my machine, maybe this evening (read: in a few hours) I can get this sorted out.

Huỳnh Trần Khanh (Jul 29 2022 at 10:52):

Damiano Testa said:

Is there a condition that kilos should be at least 4, in the question? In the solution? :upside_down:

You have to check for that.

Huỳnh Trần Khanh (Jul 29 2022 at 10:53):

if the weight is less than 4 or the weight is odd then no, otherwise yes

Huỳnh Trần Khanh (Jul 29 2022 at 10:53):

That's the solution

Huỳnh Trần Khanh (Jul 29 2022 at 10:54):

The problem statement says you need to handle any integer from 1 to 100

Damiano Testa (Jul 29 2022 at 10:54):

Right, but the proposed solution seems to give the wrong answer for input 2.

Huỳnh Trần Khanh (Jul 29 2022 at 10:56):

What do you mean? The answer is no for 2.

Damiano Testa (Jul 29 2022 at 10:57):

Indeed, but I think that the code that Henrik sent will answer yes.

Huỳnh Trần Khanh (Jul 29 2022 at 10:57):

(deleted)

Huỳnh Trần Khanh (Jul 29 2022 at 10:59):

@Henrik Böving could you fix the bug in your solution and then submit it to Codeforces?

Henrik Böving (Jul 29 2022 at 10:59):

That won't work it requires an #include <lean/lean.h> at the top

Huỳnh Trần Khanh (Jul 29 2022 at 10:59):

You can post the C code and I'll submit it for you.

Huỳnh Trần Khanh (Jul 29 2022 at 11:00):

Henrik Böving said:

That won't work it requires an #include <lean/lean.h> at the top

Yeah so you need to copy and paste the entire runtime library too...

Huỳnh Trần Khanh (Jul 29 2022 at 11:00):

Not just the header, I guess even the whole implementation...

Henrik Böving (Jul 29 2022 at 11:01):

Exactly^^

Henrik Böving (Jul 29 2022 at 11:02):

can yo use repl.it as an evaluator? I hear they are using nix-shell for their stuff and Lean does have nix support so maybe one can hack something together there.

Eric Wieser (Jul 29 2022 at 11:02):

I assume the runtime library in question is https://github.com/leanprover/lean4/tree/f6b6b36f47909fe8a089c16efdb87372154e7efa/src/runtime

Arthur Paulino (Jul 29 2022 at 11:08):

Transpiling a Lean Environment to Haskell shouldn't be too hard either.

We're doing a translation to a much simpler language called Lurk, but we have an involved step in the middle, which is content-addressing the declarations to an IR of our own: https://github.com/yatima-inc/yatima-lang

If you want you can use that as a reference and go straight to Haskell instead of taking the indirect path we are

Henrik Böving (Jul 29 2022 at 11:09):

I think where translating lean code to haskell gets tricky is when you do type computations, for example consider my (currrently compiler bugged but technically valid) code from the IR check thread:

Henrik Böving (Jul 29 2022 at 11:10):

abbrev TupleNTyp : Nat → Type 1
  | 0 => Type
  | n + 1 => Type → (TupleNTyp n)

abbrev TupleN : (n : Fin 1) → (TupleNTyp n.val)
  | 0 => Unit
--  | 1 => Solo
--  | 2 => Prod
--  | 3 => fun a b c => Prod a (Prod b c)

there is a translation for this to haskell that involves type families etc. (I got this idea from haskell code, I would have never had that idea myself my haskell foo is limited) but that is of course highly non trivial to do automatically

Arthur Paulino (Jul 29 2022 at 11:12):

I don't know if Haskell supports mutually recursive functions either

Henrik Böving (Jul 29 2022 at 11:12):

Oh of course haskell is mutually recursive by default, you can write declarations in whatever order you want

Henrik Böving (Jul 29 2022 at 11:13):

(Note: techincally not 100% true there are cases where you can trick the haskell type checker into doing certain things that do make order matter but that is besides the point)

Arthur Paulino (Jul 29 2022 at 11:13):

Well, you can always restrict your transpilation to a subset of the source language

Henrik Böving (Jul 29 2022 at 11:14):

I would also be interested to see how highly typed things like this: https://github.com/hargoniX/cpdt-lean/blob/main/Cpdt/Chapter2/Typed.lean translate, specifically the inductive definitions and again type computations.

Arthur Paulino (Jul 29 2022 at 11:16):

Yes. Remember that in the end of the day we will be dealing with expressions. So the problem kind of boils down to being able to translate those

Henrik Böving (Jul 29 2022 at 11:17):

No, an inductive is not an expression it is an entire thing on its own

Arthur Paulino (Jul 29 2022 at 11:18):

Yes, gotta encode indictives in a particular way. But doesn't Haskell have a good support for those already? That's why I mentioned Haskell

Arthur Paulino (Jul 29 2022 at 11:19):

Inductives and recursors will be tricky

Henrik Böving (Jul 29 2022 at 11:24):

AFAIK Haskell has several concepts like their normal data, their GADT data, their type family and probably more that together have at least a great feature overlap with inductive from Lean. Though I'm guessing it is possible since Coq can do code extraction to Ocaml and Haskell already, that's probably where to look at if you want to know how to do this type of stuff

Huỳnh Trần Khanh (Jul 29 2022 at 11:28):

Quick question: The Lean runtime library doesn't depend on anything else except the standard C library right?

Huỳnh Trần Khanh (Jul 29 2022 at 11:28):

I could hack something up.

Huỳnh Trần Khanh (Jul 29 2022 at 11:29):

I swear if this is true then there's a reasonable way to submit code to Codeforces.

Henrik Böving (Jul 29 2022 at 11:30):

I believe it does still use GMP for Nat though there are plans to replace that (and they might have already gone through I'm not 100% up to date regarding this)

Eric Wieser (Jul 29 2022 at 11:37):

It depends on the C++ standard library too; indeed, the runtime is written in C++ and exposes a C interface

Huỳnh Trần Khanh (Jul 29 2022 at 11:45):

Henrik Böving said:

I believe it does still use GMP for Nat though there are plans to replace that (and they might have already gone through I'm not 100% up to date regarding this)

100% gone, just checked.

Henrik Böving (Jul 29 2022 at 11:47):

Also getting back to my previous idea, I think with this https://docs.replit.com/programming-ide/nix-on-replit it should be possible to just use Sebastian's nix environment for doing Lean on repl.it so if there is some competetive programming that allows repl.it as a runtime why not use that?

Huỳnh Trần Khanh (Jul 29 2022 at 11:48):

some competitive programming

Sorry, there isn't.

Huỳnh Trần Khanh (Jul 29 2022 at 11:48):

We mostly use Codeforces.

Huỳnh Trần Khanh (Jul 29 2022 at 11:51):

I believe I can figure stuff out. Gotta get stuff installed first, brb

Huỳnh Trần Khanh (Jul 29 2022 at 11:54):

High level plan: pack everything into one single file, then put the file through some sort of transformation to make it smaller. I'll post more details when I get everything done.

Eric Wieser (Jul 29 2022 at 13:38):

Is this type of thing common? Do people often submit in languages not supported by codeforces via transpilation?

Eric Wieser (Jul 29 2022 at 13:38):

Alternatively; is this a social problem that can be solved by asking CodeForces to add support for Lean4 directly?

Huỳnh Trần Khanh (Jul 29 2022 at 13:40):

Is this type of thing common

Yes, very common.

Huỳnh Trần Khanh (Jul 29 2022 at 13:41):

It's possible to ask Codeforces to add support for Lean 4. I just need to make enough noise on the blogs section.

Huỳnh Trần Khanh (Jul 29 2022 at 13:41):

Getting them to update regularly, however, is harder.

Jason Rute (Jul 29 2022 at 13:42):

In codingames, folks would get around this by:

compiling their program to binary (for the target system I guess)
encode the binary as base85 text
put the base85 text inside a C++ file with a bit of code to decode and run it.

The primary use cases were:

using compiler flags not supported by codingames
using languages not supported by codingames
being able to work with multiple files and have them put into a single file at the end
compressing your code to get it to fit in the file size limits

It was banded from the live competitions however, since it could be used to break rules, like stealing other peoples code and obfuscate it.

Here is an example from https://www.codingame.com/forum/t/new-contests-rule/2895

#include<algorithm>
#include<fstream>
using namespace std;
constexpr char en85[]{"0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz!#$%&()*+-;<=>?@^_`{|}~"};
char de85[256];
const string Base85_Binary{"e??420s#R700000000000suY$0RR91C|p1Q00000KmY&$00000000000000000000Kma%Z0sue&000000RR911poj50000000000002M$00000002M$00000S#1CS00000S#1CS00000001BW000000RR911^@s6Fa`kt00000Fa}`&00000Fa}`&0000000000000000000000000001BW000008dcGSRZv(VKoJcV0000000{vA00{vA00IC2j{pDw4gdfE7y|%5k<e?8OBwrZ#ah<mg*02^c8;+YLrAR8lgjz+e_jGd<!bi&p*Z|gP)vrEP9f-Tqu}Hp<)I?<#{BaOLT&I^<Wp?5c7n5G$E*(xHVj?H9-}Znql!5$?bC{#O(2W2>8Ef+FPx{>SzBe&gG7Y^z87M)>shwaA>?vI>qBUm<Wd)^08_>#FsuM<@c;nQSpWbINd*8H0{{SS)*zFtp_g_lo^`+%Mlb@yS%498#6ABaeO91qYmjU%QP&Phm>-pEym?|u$ZmK8x1hiStq#=uzpO_9AfF|0_xZN7mg)V7aE<!|GZX?NgHXwdw9oq`DDnm%cvs`ng`f2eM48E>w42w1_IJH)e4DKKLw37Mv#*2w#a2Q(V|yA`Xm3A&%)l%Dx2;ZAXp}myw~a!JBCW6`*=b@mZ#-s<lG}@0=xT4;aQheLF`zSXuO1Pjd{hE=3w_Z^deO3lmYWYRwVSzjcP`uL2Bzjvs&3w})EDe-w8g_ZR~%|tR3uP@v%G3@^Vp^GN*#*DO6;uFv4IUl9;B2q$F!cmU3>Dvxx!M;jf)aZz!vC4Gw&_#8{`Ev$oEtt=k7fU)dgaf^7K<<-UUkl=l&h%*F8yJmZnhdS{QRDg<dn*@c88+BOmOY+Kp8Y3Map42~o(hWIkG+m#p`9ka9s*U9rs#GTcPTy58RW$QSQepl$9sT(&R|hj%MnqW{(8K_;L-RlgGv<V4!`Yd8#Ql6BBQBHa|bV#cE-NBBJmmA==+S1U?wF0Tq-W&}l2Ih<v^k$82s00Fk1I7D!+_DlLmZ3pyfl?Hm<JROzj0F%`=Js24Y8<b-C7u8Ey`v?t>^X!aOZ&!GE$n0gXpXDLiE&IF(p}=2$O7riG=he>HsSd6nb2ZpH9V5e+4#NUu*#dL`j>g(=6U$JSqkAe;m*8W?seFqAQtt2nub9QN{G}zVQa!h1{ubBWde6-tKEEX3f};Ds_%%m(olC~X+l9fBb_qvB7d%qxFYGvhB)ySl-6mc(7piVk$L1C!6?LsM-bGx4Kq?Vi_N7++Lr^j7Z_T!9&^TX>Z$b`iEN&!BV-<L@n8GLUb!cz~W!|L_8-Oq@pzqOi$e1(>YDtB+GC~#8K0iz=>(65ZrqrH$=W}MUQ$4`Q|7);{HDvlt$Z@j8tqRxF<8I1Il2>Re3>i>Qq-%<LE8t2h-nQrru+euZ4nU49CP<?4caPIK7bZiVj?5N%wlX6u%?{-g{*6CZj<*!3@8Z;5%bifG+G1RRp*A%_5goJw*!j=g30Kl=4$d=;r8v}<3F$o+ZcV~?yT5Xw87D)hWr2H`0#iBz0fslH3?7a|zM)PyFb}5=<jqqb91)CWNol;3p}CEx_b4Wp>g1Y4DQY=g=091dzGxgHww)>iz{pz+<(Y7?aR`K~NB7eB<-~EHPz>^f?VX3~LtUZTp)fAs;0x0G&Bnh$8R^5Tnq4&JqUhtnY5YFz72BvQIIyX;tD-6P9OCr3BhC{9%enoXD3^yq(4X%%&&LtK$3_;YUv?qx^N}P0dBy>`o-5=FVaYVxATn)qyGSArjM>;C!Ju9WFXdhLL1O3$F!e+!0GmehmaMNjXceH$D$&r{3%#fPy_N~Sw3vyu<ms04ImT(P8xhhp+A!%##E>LBA%Drj%Ls?QKN)ZJTET{UZ5p=<_?>gUDcqRbZfq7xY1wcqeq}Z{D1xyb`#f;xu0%X^x49;b&4J+&u~$Ma_*>MFeRn$iLp>AAfKC||;C6Gz?vNx^@JTxYRFR%q>aUmW3Du3=;T!NlY7P$LmGeci$bSDO#_4gfS7-~I`5pXOd>fZ!0r{YyO~x3#_6Vgl5n2S$z5J2?2r|}_k>tp)!s@)MtaFPKvl{Ks2iC{XH6lLnBNKb$a_03sv;96Sq;z%LW<~SzuvVw?zPYQTB%4Fyb{;|R;)fA=F5aCBJ}kbFsDtX#veW5zk}S_y`gj9)#yc^P-!deJ7ADXbSs~pT*()B?n@Va$(W|Q~V&x@uT=#4v5Da7IUW}Y!#5Q!DJjuSG5{yC-D!NfZ41F1sL^Eo4P3bt=O5q9iXi#QL=RNJ}s7tLFPq!BX`*Dcv8X2hk$DaS8$b`WdT3Vt61mq$M3eVK-+BEU(521X5NOMdaYbc5R1v5{iS8&_Hj<>^QtAUfTI^Zp7*D$qnwc<-^fXTlCa(^}=Jc%(jsow9j45ePA#y9rrBwB1;-A3p4+5Cj3@}HkjX_{t<Bb+*0N9$DWnMldVa$yCSQcVU&VOP=VM$7i(KR)?bqiL&r8C5|eU!xC9ib$&V%j>i|YGG{s^eCzW0>JX>@Y&`CRr5}&GC$2oHF{lE_^>9<L(6V5h6fdHog0^04i6IXu2sgxl70Fb@|(nqo(SiaywnF^l`mQ-#XATtYq9LGEg)!w;v?z}ia14AfJg4@$(T!>_UzJxUE7?vF^=Hx==#S)q%&|%R}ax+6x0okzr`g(*K)m$A}!IVy<w_HunpyRsB@`HueE;cKy%PkNsC?>b;i`6k_8*G>yp49xEnZ3N_l)7%gTPktQ|Fp4taFB7HH38aT#?FlI${WXgI<C1EJVRRAHJ(OO0&GoonC{kem$5YEVeVL3_|Zg0$L!I#CfaNeodE%4*)A#d+b+N|`huyr?H)=MQ9X3{gb<ErdJloLbJ`^x5Bl5N{?X94?3E2Pe}>hUIczO}srDmoamd&rjjh&Y?EB)7dsK0to&2r3^z?&$!1H3RAtCEs+ueRzQ5UKx$B5Pt<yn(eiKqM<=vzEplv~F_VHm0gOLSm;EU>n)UcDOG^`_R+2~enGc`SV>OH*fiL)GypF3V2!DNM6Lm|i?LEGq%X2K2Mud{%K(sQYzp7Njy0BmL&XDa4W?{Y+CosfZEIkCoeP_--$GXE1Wdb|htW9ViZ%$*_@+NDfCXqB8vEtgKS0;=cQC>`cfNv(NZH~e36ND_?Yh__*{d9@8uPL`P2h1dEBAu&atOAhhR94^XvDz&FZ;Xj9r0UQkS?e0Ew)ZNt%R12=HP?50OivG&<Y|<73#6Qr)lFt5%s$x1NE}syXtY#=T+CEq#f@{x7h-rPPo?6W1yEtba^gzmnN{PWYGYhd6Ej2u#i)V#Cn)ZUd5qx<_&)2C`ub6X#}+4@>i8xqK1Kw5E8)zCUpnIL5pZ$Su7BgLA&%D8{!8HyoaS*=u%ZniK%zn<QIW_dIIbq<uEs^KAdB+Nab-RPdM{%6)(T*+YOqlIX3dSyqYxRBfM(9D&MF7$odyVH2T7jb`r-)7cD}G^REUY|LJMB5wo(q#{l{w$bBbOxM?Fg!nNu*43})TMwEB;}U9SB#*>_~#hL>(>mhVu6@=C=<KpJ-et81uZb}qQ%m=2B4PS{{AW^E5y2D7V-_xCAk`!1ej-;SyT*MN8~9<&(43;2pvtnp3-bjHb&AiA}>mK&mYV`dB{eKGC*0^vM8dPCi})>e9)AKa}>=p|@oNSa-Bp=DVvK(|;G-Z(1S;S;Lp<Ym!+_6#)l$d1p8z_N~$>arb3F~$zi1lx{10=SX0Srr+Hb+ksi{*S;r#fNpT&k_uh=KRY|ut5MgK9-GZErU#R6)4Y0NBr!R?UAnu-bctUdr;$D#|)s5m~EGGvEYA;WM_y_v>v^m^#TP;4WRDavJ5kNCXt7T8{G;m%b63PoD|DoO>boB*$eVQ?NrDnapPnY0W<+<_%*9m%a{+Bx9Sn$m$_Am`~ShSeBOI#)1h0V`pwxck<Q;9{S#{fD@$!R?kRE2{=deeBB0_-6P>Efsqs7b0x={zf-_U`SMSeLuI;AoZi8F=0Ez{0i%=pp^ECA)vlf|IUZFT=cx7|O$(K2ib$qh}+;I|&@mJ*I>TA~!I1Yf`g2enn<rjVhKP`c+t7;Cy88Z6ooxFA3bO|+#6W|_i@BqAgLU@X~+b+6?EWD;HLMQc(9Fj?sngkA@vChDuaS^Z<-Us1C@byQ#+zbEedp5erV~OStc<`F<w&@KMR2SxMzK2wunXnZ>OJmtfAbpkeLhc$a6%q13(J()t2MIEQtFzHW<26>!Vmbk<x|tDJ1h(KPG4hmj5>KsCdd#itArx9H8n+TSHeT0WA1ixk>XmR8!ve6nHI>XDg_Jje!$r^JWRLRkzuG7sn#yv}w[...]iLi)1!WqeCjVC=8CyN#Vr#JU1S2hN6F|ig88$dQ${2>RsU$q$-{Ob#i2h$gaKJ2F5i6Fc-)tYJ<4gUUYy{q&Tip+O~F$NfTT0rE$r6*=1t;qI~lYB4xPlaVz)iar9wPVB~`39)XVZEMvjFojsPIS$*&mvXqpU&I|M;Bb~H&5MMG3yUYfj95tIj8}aVmNt^vTt4xpvCEYH`ijw>Uk#<@m=2^sYNS1mw=3TaySI{l?&9-D@Xc02X)7~|%F!4J`Ii#u^Xmk`FF9cQ>9KXIdZQ84~5Qi8-oGNL+@@QJMMM54VU|J->WHBIT{3hml=Y%;w=iZL@Hg@DFPHE`mjW0^Mq7j6)Y$+3|J?djiKcsQKkR%3>H|e<2N$=Q!Twnm0wSUHAb+sp`>gwShBr&-1m{qw%HmAR={vK+(*i*mvseI)kI8?1=(%K0?+BcX+6CAq$`kMvCB;lX7y-YmGQ!lQpmS%6#r+vXaW5F1!tPgek#;97aaQUqtkcPm6d~cu1q#U+gtuA?wR0>!`XcB>Hq7FcnUPThogQCH&&b)H6B)a&l3{0Zl<Yz#1=3A-Fo@NanO5QT_%o;8NZPME^qL=t|<Z*s2*^tc05WE;WGllM}PL-o~owzMBK?r6w@Pfl&CFP#sysIDnHWqPOeDK`ByS$q?Zq<x?Ds4<^ZYfXbpJ*#~LJ@D8I3OD)23mRnW=B#k-tXP(4fxLDR9*xB{GzF|%0<$u)3g9$ijveqjwlCZV_&@h%ci=P3pYX}>=oDkf^$ivXsvy_SkDb$MM|>Rsi)%fnf@DyfR$Ka|91*XMclg(TRA8CPKc;1O3<#05u@`zt77ovo{pl)LKaPaYcs#c{fv*7uE$8&H;)Z?jhtsI2iHZRr8#0KOg`Xp=3xVYI;ri3<tq_CW|NbXUHySZye8M=vX)o&)Bx8QF@po*2!gMX?v>IzG8%PhrzL{r>ooS0SXa6c+FXFN`7BE`M^(T6tgv&SdM|*PbYhd-E)k8u<sc&uiQh~Go#-J5YdKJE+2cb^`Z09aLXmIj6HKWz`w+$JSS>DK`7y-}^_0MWK**c5gB&A`YcN(nhdQp1Ad<I2YX|H9IK+X{B>5#6A{Ms9g25Q;4rlR9t=xG&A1FXTOst{~80uh(`>)S{l#~rQGZ<D5+b~+gINCsKuhs+$uYmQ(v>aWu4@wVmW`CNt<`C$4$Zf&V@BThXUR6ki_5-K3&Cb)MeXVz}6xhoFQ&C^PQli3^E><yHtqd2t7$1Or7{)56gwBqoM)Z$?jB-yCA6?uYBo%~JRCP&l6=u4w?3WKIt(<GdfHq>ewZts%8Y9+t;GT*sZ9z_{noz17yMNs&S4^{&WT^mZN~7oKT^=>o$xGbqdGa2+pDhHlw4lkTHEbbvhX4QobP50f7XSbN4gdfE7y|$RaDDy%u8^TX6TMS5owNdC${YZw2LJ%g0RR9F0000O0{{RF)HPN3(ySE8#o?IA)wc%1>?tG*2{B(?NvHVKVAzcM-;cM5YWS!GP?En(sJTAQ6wsXJMD}8qP`4P}z1KP?1^YlaF4kSTGWN)*nwGRS3}_dkH2(SpZtXPr;<^VH8Q1#C0dlPHT_1&gg014cxFe2bqi8n_Gn4Iiw~vkA$^2Fj40m2{a;44G4NecD-nDyM9$@r7{ZWsDu$PDLT>E8FtHj`o-nW~_qehB~Z73velzeNtwRDpJ#DO2rxEn5O4qHJ*K~kc+LV!1>dAFeVkpf(krq?sV?=ya`i>}ZeZt6NkaJE)15eu$h-zIWZ!|rM=36$#t<^)w7PMAxmjN0f#tI=wkGCsM_oLhbVor4XO8^m?sel_a#O=~FCX6TjZ7I)MN+oMI0+(<FnGS~iaL4|0Fa0_4xm0w+U4HOEs&a@&WY_pp%Ushf{Rs2d-IzA5CBL3PQYqki1gDK>+h9$EhC<svxCfgEc554;~8@Cmckj@*CDUPKaz>X)CUOg#l7EFMcl74&{k@cM~Wc%7DRpYmtr3TpMAhHnR5T7SZ8Xju3qe|R8%6d#+!q%T7;=I9G!5Nb{HKT-q00000RZv(V00000RZv(V4Hgaxj3w4*B2_z+s0RQ5%>e)a00{vANd*90yZ`_I"};
string decode_85(const string &base85_string){string out;size_t str_ptr{0};while(str_ptr<base85_string.size()){unsigned int acc{0};for(int i=0;i<5;++i){unsigned char ch=base85_string[str_ptr++];int de{de85[ch]};acc=acc*85+de;}string sub;for(int i=0;i<4;++i){int val=acc%256;acc/=256;sub+=static_cast<char>(val);}reverse(sub.begin(),sub.end());out+=sub;}return out;}
int main(){for(int i=0;i<85;i++){int ch{en85[i]};de85[ch]=i;}const string Program_Binary{decode_85(Base85_Binary)};ofstream Program_File("Binary",ios::binary | ios::trunc);
Program_File.write(Program_Binary.c_str(),Program_Binary.size());
Program_File.close();
system("chmod a+x Binary");system("./Binary");};

Huỳnh Trần Khanh (Jul 29 2022 at 13:43):

Good thing it's not banned on Codeforces provided that the original source code is included in a comment.

Jason Rute (Jul 29 2022 at 13:54):

Oh, I see, you already considered this above.

Eric Wieser (Jul 29 2022 at 14:03):

I don't see where that was mentioned above; mind linking the message?

Huỳnh Trần Khanh (Jul 29 2022 at 14:08):

Is there a standard way to cross compile Lean code for another platform, say, Windows? If not, I'll keep monkey patching stuff.

Huỳnh Trần Khanh (Jul 29 2022 at 14:11):

My plan is I'll manually compile the runtime, then I'll replace the leanc binary with a dumb script that calls the cross compilation toolchain.

Locria Cyber (Jul 29 2022 at 14:11):

Have you heard of a C compiler that simply merge all files?

Locria Cyber (Jul 29 2022 at 14:12):

somebody used it to sumbit Nim script as C

Locria Cyber (Jul 29 2022 at 14:12):

Can't remember the name. There is one for C++ as well.

Huỳnh Trần Khanh (Jul 29 2022 at 14:13):

I've seen people use Python scripts that topologically sort #includes...

Huỳnh Trần Khanh (Jul 29 2022 at 14:14):

There is one in the AtCoder Library as well.

Huỳnh Trần Khanh (Jul 29 2022 at 14:17):

This stuff is crazy I think my brain is melting

Jason Rute (Jul 29 2022 at 14:17):

When I did programming contests in python, I had a cool tool of mine which turned a big project into a single file. https://github.com/jasonrute/modulize

Huỳnh Trần Khanh (Jul 29 2022 at 14:19):

Rust has cargo-equip

Jason Rute (Jul 29 2022 at 14:22):

Eric Wieser said:

I don't see where that was mentioned above; mind linking the message?

I was just referring to Mac mentioning that you could use the compiled c code and ~~Huynh~~ Khanh responding that it requires also including the runtime libraries which may not be easy. (The base85 stuff wasn’t explicitly mentioned, but it also seems ~~Huynh~~ Khanh is familiar with the standard tricks in this area.)