talk.tryitonline.net

1:14 AM

@Dennis they auto-build every day

1:36 AM

@AmokHuginnsson Done.

AmokHuginnsson

@Dennis Thank you

@LeakyNun Nice. How can I test if it's working? tio.run/##y0lNzPv/… appears to have been deprecated.

@Dennis tio.run/##y0lNzPsPArq6ZalFxZn5eQA

@LeakyNun Sorry, that wasn't clear. I want to test if Lean finds the mathlib.

@Dennis then your code seems to indicate that it's fine

1:51 AM

That's not on the test server. The latest version of mathlib doesn't have analysis/real anymore.

/home/runner/.code.tio:1:0: error: file 'analysis/real' not found in the LEAN_PATH
/home/runner/.code.tio:1:0: error: invalid import: analysis.real
could not resolve import: analysis.real
/home/runner/.code.tio:2:12: error: unknown identifier 'real'

This is with both the self-compiled mathlib and the nightly.

analysis only has calculus, complex, and normed_space.

tio.run/##y0lNzPv/…

import data.real.basic
#check (2 : real)

Hm, still broken with both.

but you said that "analysis only has calculus" etc

which means you can access mathlib

I can. Lean can't.

Ah, the path structure changed. I have to append a /src to the Lean path now...

I'll have to try again when my internet comes back. Not having the best day...

2:23 AM

The path adjustment worked just fine for the self-compiled version. The nightly's been running for three minutes now, without producing any output.

Uh, the latest nightly build of Lean in from January...

My timer aborted it after 10 minutes...

OK, it works if I use github.com/leanprover/lean instead of github.com/leanprover/lean-nightly.

Full builds just became six hours shorter.

@LeakyNun Thanks!

cool

6 hours later…

Cows quack

8:10 AM

@Dennis thanks

2 hours later…

9:43 AM

@Dennis Can you update Dyalog APL?

3 hours later…

12:52 PM

@Adám Done.

@Dennis Cool, thanks.

2 hours later…

2:37 PM

Does anyone here have experience with Maven?

2:56 PM

To the extent that letting my IDE manage absolutely absolutely everything related to it is experience

3:08 PM

I think I can use gradle.

Or I could, if I knew how.

Welp, there's always building from source, I guess.

@Dennis What are you trying to do with them, anyway?

Dyvil stopped making GitHub releases, presumably because that was too accessible.

Compiling it from master worked well, but now I can't figure out how to run it.

Did compiling produce a main.class file anywhere?

I got that far, but it can't find other stuff.

Exception in thread "main" java.lang.NoClassDefFoundError: dyvilx/tools/BasicTool

@Dennis If the other stuff does actually exist somewhere, you can tell java where to find it with the -cp ("class path") flag

3:23 PM

Yeah, I'm trying to figure out where it got packaged into.

The release used to be a single jar, which was easier.

3:40 PM

Seems to be working.

4:14 PM

@ais523 I'm trying to update wasm. It seems to work, but the old Hello World is broken.

Error parsing WebAssembly text file:
/tmp/PEvwlT1skC/a.wast:11:2: legacy instruction name: requires the legacy-instr-name feature.
 get_global $stdout

Any idea what we're supposed to use instead of get_global?

legacy-instr-name seems to exist only for running, not assembling...

4:27 PM

Hm , even with "--enable", "legacy-instr-names", the output is just empty...

Nevermind, found a new Hello World here. github.com/WAVM/WAVM/blob/master/Examples/helloworld.wast

A lot more complicated than the old one...

I suppose WaWrapper's Imports.pm is supposed to help with that, but I don't know how to take advantage of it, nor it it still works with all the changes to WAVM.

1 hour later…

5:57 PM

@Dennis Addition is hard: TIO hosts 260 practical and 420 recreational programming languages, for a total of 681 languages.

Heh, there's a language that's currently unlisted, so it's counted for neither category.

Ooh, mystery languages…

tio.run/#pyret

It's unlisted because it's broken.

@Dennis Wouldn't it be an idea to compute {total} from {practical} and {recreational}?

For the current format, sure. The original idea was to have far more categories.

Like an APL category, for example.

As with so many ideas, I never got around to do that.

List of programming languages by type

6:07 PM

@Dennis That sounds interesting. So you'd classify languages by type? Like

This is a list of notable programming languages, grouped by type. Since there is no overarching classification scheme for programming languages, in many cases, a language will be listed under multiple headings. == Array languages == Array programming (also known as vector or multidimensional) languages generalize operations on scalars to apply transparently to vectors, matrices, and higher-dimensional arrays. == Assembly languages == Assembly languages directly correspond to a machine language (see below) so machine code instructions appear in a form understandable by humans. Assembly languages...