Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #135677
| Path | csiph.com!eternal-september.org!feeder.eternal-september.org!nntp.eternal-september.org!.POSTED!not-for-mail |
|---|---|
| From | Paul Rubin <no.email@nospam.invalid> |
| Newsgroups | comp.lang.forth |
| Subject | Re: First result in riscv optimiser |
| Date | Fri, 11 Sep 2026 17:09:19 -0700 |
| Organization | A noiseless patient Spider |
| Lines | 9 |
| Message-ID | <87cxujjpow.fsf@nightsong.com> (permalink) |
| References | <nnd$172defd2$1b2df6f6@e430673098f06a19> <87ecf96ljg.fsf@debian> <nnd$23c5006f$6f768ed1@9c6c99f017e8c6d5> <87y0dcgvxf.fsf@debian> <nnd$2a0f5231$3093e519@df6cdc0aa2637ff7> <877bksdpui.fsf@debian> |
| MIME-Version | 1.0 |
| Content-Type | text/plain |
| Injection-Date | Sat, 12 Sep 2026 00:09:20 +0000 (UTC) |
| Injection-Info | dont-email.me; logging-data="3510250"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX197LukzWXpoMGqdIlmbatOn"; posting-host="605061d606f2312cb00f7b420c549432" |
| User-Agent | Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) |
| Cancel-Lock | sha1:QR12rjZdh3a2KcEy3v6lpVi+qwc= sha1:5694gKafkoW+5ynLfOc02Orxom0= sha256:lpKhHDIzHTDWCsY51ct7f7WWz83zQySCC3M88qTbGOA= sha1:1Vj7KeSKSBEePvEpIV4MmBcFh/c= sha256:C35jPOIsDNnIIK72rqzQhPtsVKAMOnpxbxA9ocqe/IA= |
| Xref | csiph.com comp.lang.forth:135677 |
Show key headers only | View raw
Kragen Javier Sitaker <kragen@canonical.org> writes: >> I have 106 peephole patterns, some quite complicated. > How confident are you that all 106 are correct? It's sometimes possible to use SAT solvers to prove that two code sequences are equivalent, without much human input. There are also formal models of RISC-V that you can put into a proof assistant. Or these days maybe you can throw the whole set into an LLM and ask for formal proofs.
Back to comp.lang.forth | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-01 10:49 +0200
Re: First result in riscv optimiser anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2026-09-01 15:33 +0000
Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-01 18:54 +0200
Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-02 11:18 +0200
Re: First result in riscv optimiser Kragen Javier Sitaker <kragen@canonical.org> - 2026-09-04 13:14 -0300
Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-05 13:06 +0200
Re: First result in riscv optimiser Kragen Javier Sitaker <kragen@canonical.org> - 2026-09-08 02:21 -0300
Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-08 12:38 +0200
Re: First result in riscv optimiser Kragen Javier Sitaker <kragen@canonical.org> - 2026-09-11 07:50 -0300
Re: First result in riscv optimiser Paul Rubin <no.email@nospam.invalid> - 2026-09-11 17:09 -0700
Re: First result in riscv optimiser albert@spenarnc.xs4all.nl - 2026-09-13 14:03 +0200
Re: First result in riscv optimiser antispam@fricas.org (Waldek Hebisch) - 2026-09-13 02:53 +0000
csiph-web