<cedb>
"This expression has type unit t but an expression was expected of type unit because it is in the result of a conditional with no else branch"
<cedb>
what i dont get is the error goes away when i remove the let binding
<discocaml>
<yawaramin> that code snippet by itself works fine even with the let-binding. the problem is somewhere else
<cedb>
its in the context of Lwt_main.run theres lwt code in there
myrkraverk has joined #ocaml
<discocaml>
<Kali> new guess: you have an unnecessary semicolon in the then-clause that is making the if statement be treated like a branchless if, which must have a return type of unit
<discocaml>
<yawaramin> there we go: `let%lwt machine = ...` this code means that everything after it is an Lwt promise, so it won't have type `unit`, hence `if` without `else` clause won't work
myrkraverk_ has quit [Ping timeout: 252 seconds]
<discocaml>
<Kali> oh, yeah, that's probably it
<cedb>
it works when theres no let though isnt that weird
<discocaml>
<Kali> that's likely an error with the %lwt preprocessor
<cedb>
hmm, thats a strong statement
<discocaml>
<Kali> try using let* syntax instead of %let? if it's available on the version you're using
<discocaml>
<yawaramin> can you give us a minimal repro that shows it working then?
<cedb>
sidechannel question this code has a lot of subprocess runs, and often i want to run somethign only if a condition is true, is there a clean way to do this if i end up using lwt, even if just for cohttp stuff
<cedb>
yawaramin ahh okay thanks
<cedb>
i thought id try ocaml for scripting, being noobish in it doesnt help but damn tough choice for that
<dmbaturin>
I do sometimes use ocaml for scripting. It works quite well in that role.
<cedb>
dmbaturin: how do you deal with subprocesses? this has been giving me a headache
<dmbaturin>
cedb: Ah, I usually don't do a lot of that. But `Unix.open_process_*` aren't that annoying to use, in my experience. Although some higher-level wrappers might not harm.
<cedb>
and it works if i add an else clause hmm this is super weird
<discocaml>
<yawaramin> that's normal, else clause is needed if the if branch doesn't evaluate to unit type
<cedb>
so is there a way adding bindings changes the type of the if branch?
<discocaml>
<yawaramin> not if the binding expression evaluates to the same type as the bare expression without the binding
myrkraverk_ has joined #ocaml
myrkraverk has quit [Ping timeout: 265 seconds]
polykernel has quit [Remote host closed the connection]
polykernel has joined #ocaml
deavmi has quit [Ping timeout: 272 seconds]
Johann has quit [Ping timeout: 248 seconds]
deavmi has joined #ocaml
Johann has joined #ocaml
pi3ce has joined #ocaml
wbooze has quit [Ping timeout: 272 seconds]
agentcasey has joined #ocaml
troydm has quit [Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset]
troydm has joined #ocaml
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 265 seconds]
Humean has quit [Ping timeout: 260 seconds]
Haudegen has joined #ocaml
wbooze has joined #ocaml
chrisz has joined #ocaml
LainIwakura has joined #ocaml
bartholin has joined #ocaml
LainIwakura has quit [Quit: Client closed]
hidjgr has quit [Quit: WeeChat 4.4.2]
hidjgr has joined #ocaml
hidjgr has quit [Changing host]
hidjgr has joined #ocaml
olle has joined #ocaml
myrkraverk_ has joined #ocaml
myrkraverk has quit [Ping timeout: 265 seconds]
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 265 seconds]
wingsorc has joined #ocaml
Tuplanolla has joined #ocaml
chrisz has quit [Ping timeout: 244 seconds]
chrisz has joined #ocaml
wickedshell has quit [Ping timeout: 260 seconds]
olle has quit [Ping timeout: 252 seconds]
myrkraverk_ has joined #ocaml
myrkraverk has quit [Ping timeout: 260 seconds]
<discocaml>
<argbet> Hi guys!
<discocaml>
<argbet> Hi guys! 👋
<discocaml>
<argbet> I got interested OCaml because it seems like it's the most ideal language to be able and formally verify, is that right?
<discocaml>
<argbet> I got interested OCaml because it seems like it's the most ideal language to be able and *formally verify*, is that right?
<discocaml>
<argbet> Maybe alongside Haskell
<discocaml>
<contificate> formally verify properties about programs written in OCaml or properties about the OCaml language and implementation itself? both are difficult
<discocaml>
<yawaramin> might actually be easier in eg Java because of things like JML
<discocaml>
<contificate> does JML verify anything?
<discocaml>
<contificate> doesn't it just compile in assertions at each point so it fails at runtime, but if you never test that path because of another logic bug, the implementation may still just be incorrect
wickedshell has joined #ocaml
<discocaml>
<yawaramin> > OpenJML is capable of checking Java programs annotated with specifications in the Java Modeling Language and provides robust support for many of JML's features. That is, OpenJML does deductive program verification to check that a program's implmentation (in Java) satisfies its specification (in JML). OpenJML can also perform runtime-assertion-checking.
<discocaml>
<contificate> I'd maybe try Why3 to stay within the ML family
<discocaml>
<contificate> but it's nice that you can do some static stuff with JML
<discocaml>
<yawaramin> actually, on that note, it's possible to use Coq/Rocq to formally verify stuff and then compile the verified code to OCaml
Humean has joined #ocaml
<discocaml>
<edhebi> this is an assumption I've been having but I feel I should check it, am I correct that non-repl ocaml code doesn't have meaningfull line breaks at all other than line comments and string literals ?
<discocaml>
<edhebi> this is an assumption I've been having but I feel I should check it, am I correct that non-repl ocaml code doesn't have meaningful line breaks at all other than line comments and string literals ?
<discocaml>
<edhebi> well I guess repl doesn't either, hence the need for ;;
<discocaml>
<octachron> White spaces only affect tokenisation indeed (and there are no difference between white spaces).
<discocaml>
<yawaramin> OCaml code is whitespace-insensitive
<discocaml>
<edhebi> this is really elegant
<discocaml>
<._null._> (OCaml doesn't have line comments, and newlines are interpreted as-is in strings)
<discocaml>
<edhebi> wdym ocaml doesn't have line comments ?
<discocaml>
<edhebi> oh yeah, my brain farted here, nvm
<discocaml>
<._null._> OCaml has only has block comments
<discocaml>
<edhebi> yeah, I'm writing non-ocaml right now and got pretty confused
<discocaml>
<edhebi> is there a reason btw for that lack of line comments, other than not feeling the need to add them ?
<discocaml>
<edhebi> it makes commenting in/out blocks of code kind of bothersome
<discocaml>
<yawaramin> it makes it easy. just add a comment start symbol at the start of the block and a comment end symbol at the end. OCaml also supports nested comments
<discocaml>
<edhebi> eh, I'm just so used to doing that with line comments that my muscle memory is working against me ^^'
<discocaml>
<deepspacejohn> All of the major editors should have a (cross-language) shortcut to comment out a range of lines anyway.
<discocaml>
<yawaramin> eg VSCode with the OCaml Platform extension has `Cmd-/` which works with a block of code
Serpent7776 has joined #ocaml
<discocaml>
<dubious245> That is twice as many symbols as //
<discocaml>
<yawaramin> it's less than `//` on every...single...line
<discocaml>
<dubious245> Yeah but you can do /* */ when you need a block comment.
<discocaml>
<dubious245> You can have both.
<discocaml>
<yawaramin> i was replying to the person saying that OCaml comments make it harder to comment out blocks of code
<discocaml>
<Kali> re ocaml formal verification: definitely not, if you're looking to formally verify ocaml programs, use a proof-oriented language that compiles to ocaml like coq, why3, or f*
<discocaml>
<dubious245> I interpretted blocks of code after talking about line comments specifically as commenting out a line.
<discocaml>
<Kali> i would personally recommend why3 out of those since it had the best documentation and ease of use for me
<discocaml>
<Kali> and its syntax is also closest to ocaml's (although the others are moderately close too as derivatives of ML)
<discocaml>
<Kali> but using ocaml itself for formal verification is not really much better than any other language, it's impure and non-total and does not have a proof system
<discocaml>
<Kali> even something like Java or C would be better than OCaml at this because at least they have 3rd party tools for static verification even if it isn't part of the language
Haudegen has quit [Quit: Bin weg.]
<discocaml>
<edhebi> hey, muscle memory has me often commenting in/out a single line, and now with block comment its two actions :p
<discocaml>
<edhebi> and yes the issue is me not taking full advantage of my tools, I fully aggree
Haudegen has joined #ocaml
gingerpaaji has joined #ocaml
<gingerpaaji>
hey there
<gingerpaaji>
I want to contribute to ocaml
<gingerpaaji>
i am learning the version definitions right now and trying to understand the ocaml_version.m4 file
gingerpaaji has quit [Changing host]
gingerpaaji has joined #ocaml
<discocaml>
<argbet> The former
myrkraverk has joined #ocaml
<discocaml>
<argbet> That's what I meant, sorry if it was badly said.
<discocaml>
<argbet>
<discocaml>
<argbet> But yeah, the reason I'm looking into OCaml is because I can use Coq which could be translated over to OCaml, so your codebase would basically now be in OCaml
<discocaml>
<argbet> That's what I meant, sorry if it was badly said.
<discocaml>
<argbet>
<discocaml>
<argbet> But yeah, the reason I'm looking into OCaml is because I can use Coq which could be translated over to OCaml, so your codebase would basically now be in OCaml.
<discocaml>
<argbet> Using like, Java or JS or Rust would be more difficult cuz Coq doesn't translate over to those languages?
myrkraverk_ has quit [Ping timeout: 248 seconds]
<discocaml>
<contificate> extraction to OCaml from Coq is different from proving the correctness of an OCaml program
<discocaml>
<contificate> sorry, Rocq* 🥴
<discocaml>
<argbet> Can I use a mix of Rust and formally verified OCaml?
<discocaml>
<argbet>
<discocaml>
<argbet> The formal verification for critical stuff and Rust for everything else
<discocaml>
<argbet> Ah, fair enough
<discocaml>
<argbet> I'm guessing the former is easier than the latter right
<discocaml>
<contificate> I'm not overly familiar with people proving the correctness of OCaml programs
<discocaml>
<contificate> but I do hear about extraction to OCaml from Rocq
gingerpaaji has quit [Quit: Client closed]
<discocaml>
<argbet> Yeah, that's why I'm interested in OCaml, cuz it's the only language (besides Haskell) which could be extracted from Rocq
<discocaml>
<argbet> I don't know if there are other theorem provers which extract to other languages like Java, Rust, ..etc
<discocaml>
<octachron> F* and Lean can extract to C. Note however that the extraction language is mostly relevant in term of how you interface with the extracted code.
<discocaml>
<octachron> Rocq extracted to OCaml is using OCaml as a compilation middle-end, and not really OCaml the language.
<discocaml>
<yawaramin> technically, you can use a mix of anything and anything 🙂
<discocaml>
<argbet> So those theorem provers extract to C but when it comes to the *correctness* of a program, OCaml is better in that regard?
<discocaml>
<argbet> Hmm, I'm not sure so what the implication of this would be?
hidjgr has quit [Quit: WeeChat 4.4.2]
<dh`>
eh?
<dh`>
you can extract from rocq to whatever you want, it's programmable
<dh`>
extracting to C doesn't work very well because of allocation issues, but I think people do python
<dh`>
however, it's
<dh`>
oops
<discocaml>
<octachron> For code proven correct, the extraction language is mostly irrelevant for correctness. One could even argue that extracting to C and using Compcert C semantics would be a "more correct result" because it removes the footnotes "if the extraction is correct and is compiled correctly".
<dh`>
no, only the "compiled correctly" part of that
<dh`>
maybe if you carry proofs through to the output but I think that would be a research project
cedb has quit [Quit: WeeChat 4.6.1]
<discocaml>
<octachron> Oh yes, I meant if one had a fully proven extraction chain
<dh`>
there was a paper on that recently :-) but that extraction works differently and I'm not sure what the odds of emitting C from it might be
<dh`>
...plus realistically if you can emit C, you can emit asm and then the downstream pipeline is much simpler
<dh`>
it occurs to me that one could maybe invent a machine whose asm is specifically suitable for extraction
<dh`>
but this has wandered well off topic
<discocaml>
<froyo> some ocaml data structures are proven correct, I think the trees that back Set and Map are, contificate
<discocaml>
<froyo> and the 5.0+ gc was recently formalized in F* there was a paper on that
<discocaml>
<._null._> Do you mean that the algorithm was proven correct, or that the implementation was mirrored in a provable language ?
<discocaml>
<froyo> I'm unsure
<discocaml>
<froyo> I didn't keep a mental note of the details
<discocaml>
<froyo> read it in passing
<discocaml>
<contificate> yes but it's not like they inline annotate stuff in OCaml to then extract proof obligations
<discocaml>
<froyo> > One of the verified implementation is the actual code for sets and maps from the Objective Caml standard library. The formalization refines the informal specifications of these libraries into formal ones. The process of verification exhibited two small errors in the balancing scheme, which have been fixed and then verified.
<discocaml>
<froyo> So I guess at least the balancing algorithm was proven
<discocaml>
<octachron> No, the OCaml 5.x GC is not formalized, KC publication was about formalizing a non-concurrent GC in F* for OCaml 4.14 (without reaching feature parity with the actual GC).
<discocaml>
<froyo> (at most the whole module)
<discocaml>
<._null._> Proving an algorithm correct is very common, mirroring is better but it's only as trustworthy as the belief that the translation is faithful
<discocaml>
<froyo> that's the one I was referring to yeah (minus the comma in the url)
<discocaml>
<froyo> I was under the impression it was 5's GC
<discocaml>
<octachron> Unfortunately, I can confirm that the GC code has not been recently replaced by a fully correct version.
<discocaml>
<froyo> > The memory manager that we describe corresponds to the GC in OCaml version 4.14.1. OCaml 5 has introduced a concurrent and a parallel GC [19 ], the details of which we omit as it is not in the scope of the current work.
<discocaml>
<froyo> considering formalizing the gc is already going above and beyond :)
<discocaml>
<froyo> it's a great piece of engineering just as it is
<discocaml>
<froyo> that many years of work is nothing to scoff at
<discocaml>
<diligentclerk> We can get into the fine details of what it means for the extraction to be verified but I think that we can call this a "correct extraction", so the contingency is on whether the OCaml runtime executes this untyped lambda calculus correctly https://github.com/MetaRocq/rocq-verified-extraction
Serpent7776 has quit [Ping timeout: 276 seconds]
chrisz has quit [Ping timeout: 268 seconds]
bartholin has quit [Quit: Leaving]
wbooze_ has joined #ocaml
wbooze_ has quit [Max SendQ exceeded]
myrkraverk_ has joined #ocaml
wbooze has joined #ocaml
wbooze has quit [Killed (copper.libera.chat (Nickname regained by services))]
wbooze has quit [Max SendQ exceeded]
wbooze has joined #ocaml
chrisz has joined #ocaml
myrkraverk has quit [Ping timeout: 252 seconds]
<discocaml>
<dubious245> Wow you really notice how much slower other compilers are when you switch from Ocaml to something else.
<discocaml>
<dubious245> It's not even a big code base by any means.
<discocaml>
<edhebi> what are you switching to ?
<discocaml>
<dubious245> C#
<discocaml>
<edhebi> ye, most of the dotnet compilers aren't fast
<discocaml>
<yawaramin> i write Scala in my day job lol. OCaml feels like magic
laina has joined #ocaml
<dh`>
indeed you do, ocamlopt being fast is a real asset
<dh`>
ghc is ass slow by comparison, and rustc is quite a bit worse
laina has quit [Ping timeout: 240 seconds]
broski has joined #ocaml
broski has quit [Ping timeout: 240 seconds]
broski28 has joined #ocaml
broskia has joined #ocaml
oisota1 has joined #ocaml
oisota has quit [Ping timeout: 260 seconds]
oisota1 is now known as oisota
Tuplanolla has quit [Quit: Leaving.]
tremon has quit [Quit: getting boxed in]
broski28 has quit [Quit: Client closed]
broskia has quit [Quit: Client closed]
<discocaml>
<shawnfrostx> rustc really makes that xkcd compiling comic from 2007 relevant again
<discocaml>
<diligentclerk> Is scala 3 much better?