Two new bindings on GitHub: ada-imgui + ada-stb, and a questionr

> Two new bindings on GitHub, both MIT:

>

> **[ada-imgui]( GitHub - the-dark-factory/ada-imgui: Dear ImGui 的 Ada 绑定 | Ada bindings to Dear ImGui via cimgui. Immediate-mode GUI. 中文/EN · GitHub )** — Ada

> bindings to Dear ImGui via cimgui. v0.1-dev. Smoke test

> verifies the C++ side links cleanly (Context lifecycle +

> style hooks). The wider widget surface is bound but not

> exercised by the smoke test yet; that’s because the meaningful

> exercise needs a windowing backend (GLFW / SDL / etc.) and

> binding one of those is a separate problem. CHARTER and

> AUDIT files in the repo are honest about what’s tested

> end-to-end and what’s plausible-but-untested.

>

> **[ada-stb]( GitHub - the-dark-factory/ada-stb: Sean Barrett STB 库的 Ada 绑定 | Ada bindings to Sean Barrett's STB header-only utility collection. Image loading and more. 中文/EN · GitHub )** — Ada

> bindings to Sean Barrett’s STB header-only utility headers.

> v0.1-dev. First sub-binding is `Stb.Image` (PNG/JPG/BMP/GIF/

> PSD/TGA/HDR loading). Smoke test loads a real PNG and

> validates dimensions + the allocator hand-off on free.

> Per-header child packages under one umbrella; next planned

> additions are `Stb.Image_Write`, `Stb.Truetype`,

> `Stb.Rect_Pack`.

>

> Both are early. Both build + run on macOS today; Linux is

> untested but the code is portable.

>

> **The reason for posting:** the Projects to Work on list on

> ada-lang.io was the starting point for these two picks. But

> that list is a snapshot, and most static-doc lists go stale

> faster than the community moves. So before picking the next

> piece of work — I’d like to hear what you’d actually reach

> for if you were starting an Ada project today.

This post was caught in the spam filter and the moderation team is unsure whether to allow obviously AI-generated content. I’d like to hear what the community thinks.

I am fine with AI generated content as long as it is not marketing, is not misleading, and most important is focused on Ada, especially if it helps fill a need (eg useful bindings)

I apologise for the splash, I just intended to inform the community of the release of several libraries. I went for an AI announcement as I wanted the note to have all the information.

The note may have all the information, but is not really easy to read.

I recommend to review potential future announcements, and to clean up the layout.

I’ll prefix this by saying that I’m using coding agents for my own Ada learning and coding.

The post leaves an impression of “lowest possible effort” on me, on the same level as most of the spam I see. My expectations on useful contributions to this community are very different.

Please do better next time.

Being a little late to the party, I think it is alright to share things made with the assist of AI. However, if the project is completely AI generated without active human supervision, it will probably be of little to no use.

Also, I will point out that the poster’s account on initial appearance looks to me a bit suspect.
I am most probably wrong on this so please do not take my word for it.

1 Like

I thought the same so I looked into it and found out that Tony Gair has a company named “The Dark Factory” with only him and Claude AI as employees. (Nothing wrong with that. Making a company is probably hard. I have no experience with that).

It seams to me that everything is AI generated, even the site explaining how he uses ai. (See Built with Claude · The Dark Factory)
The only thing he adds is the prompt and occasional manual intervention (as far as I could understand the wordy and presumably AI written article)

Excerpt from the Website

In practice.

  • If the work is “demonstrate that a tool can produce SPARK from Fortran,” calling Claude directly is enough. We have nothing to say against that.
  • If the work is “ship verified software a safety reviewer can sign off — with a reproducible audit trail showing how it was produced,” that is the factory’s job, and the gap is what we sell.

TBH. I’m really not a fan of AI generated code. Especially not if it has only been done to “Pimp up” ones CV. It’s now the third time I see someone generate Ada code just to put it on their Portfolio. And here the entire Portfolio is made up of AI generated Ada Projects. (See Portfolio — The Dark Factory)

I would consider this spam as it’s a low effort project. Everyone can just generate code now, there is no real work involved, it mostly exists to advertise himself and it takes resources from other Ada developers (See stb_ada 0.1.0 · Pull Request #1948#pullrequestreview-4449534711 · alire-project/alire-index).


On a side note

I tried running the example in Verifier kit — The Dark Factory and it seams to be broken. (At least for me)

➜  Downloads tar xzf dark-factory-verifier.tar.gz 
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
tar: Ignoring unknown extended header keyword 'LIBARCHIVE.xattr.com.apple.provenance'
➜  Downloads cd dark-factory-verifier && make all
Running gnatprove --level=1 on 15 routines...
routine                obligations   unproved  discharge%%
---                           ---        ---          ---
[blas-ddot]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
blas-ddot                       0          0            %
[blas-daxpy]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
blas-daxpy                      0          0            %
[blas-dscal]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
blas-dscal                      0          0            %
[blas-dnrm2]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
blas-dnrm2                      0          0            %
[blas-dgemv]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
blas-dgemv                      0          0            %
[blas-dgemm]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
blas-dgemm                      0          0            %
[fftpack-cfftf]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
fftpack-cfftf                   0          0            %
[lapack-dpotrf]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
lapack-dpotrf                   0          0            %
[lapack-dgeqrf]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
lapack-dgeqrf                   0          0            %
[lapack-dgetrf]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
lapack-dgetrf                   0          0            %
[phase3-relu]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
phase3-relu                     0          0            %
[phase3-max_pool]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
phase3-max_pool                 0          0            %
[phase3-layernorm]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
phase3-layernorm                0          0            %
[phase3-conv2d_fp64]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
phase3-conv2d_fp64              0          0            %
[phase3-int8-matmul]
grep: obj/gnatprove/gnatprove.out: No such file or directory
grep: obj/gnatprove/gnatprove.out: No such file or directory
awk: cmd. line:1: error: division by zero attempted
phase3-int8-matmul              0          0            %

Compare against the published numbers:
  diff expected-results.txt actual-results.txt
➜  dark-factory-verifier diff expected-results.txt actual-results.txt 
1,31c1,17
< routine                obligations   unproved   discharge%
< ---                            ---        ---          ---
< blas-ddot                      349         22         93.7%
< blas-daxpy                     294         15         94.9%
< blas-dscal                     216         25         88.4%
< blas-dnrm2                     292         23         92.1%
< blas-dgemv                     399         46         88.5%
< blas-dgemm                     449         79         82.4%
< fftpack-cfftf                  661         48         92.7%
< lapack-dpotrf                  430         48         88.8%
< lapack-dgeqrf                  432         54         87.5%
< lapack-dgetrf                  528         34         93.6%
< phase3-relu                    367         22         94.0%
< phase3-max_pool                434         48         88.9%
< phase3-layernorm               405         23         94.3%
< phase3-conv2d_fp64             489         28         94.3%
< phase3-int8-matmul             559         24         96.0%
< 
< Notes:
< - Numbers are at gnatprove --level=1 against the .ads/.adb pairs
<   in routines/<name>/.
< - The "unproved" column is the count of proof obligations the
<   prover could not discharge at this level. None are body-correctness
<   failures on the routines in this kit; see README.md for the
<   three classes of unproved residue.
< - blas-dger and phase3-int8-conv2d are on the public /results/ page
<   but are NOT in this kit — their gnatprove outputs were not saved
<   during the last rerun and are queued for re-execution.
< - Phase 4 (softmax, attention, transformer block) are on the public
<   /results/ page but not yet in this kit — they are very new and
<   their published artefacts will be added in a kit refresh shortly.
---
> routine                obligations   unproved  discharge%%
> ---                           ---        ---          ---
> blas-ddot                       0          0            %
> blas-daxpy                      0          0            %
> blas-dscal                      0          0            %
> blas-dnrm2                      0          0            %
> blas-dgemv                      0          0            %
> blas-dgemm                      0          0            %
> fftpack-cfftf                   0          0            %
> lapack-dpotrf                   0          0            %
> lapack-dgeqrf                   0          0            %
> lapack-dgetrf                   0          0            %
> phase3-relu                     0          0            %
> phase3-max_pool                 0          0            %
> phase3-layernorm                0          0            %
> phase3-conv2d_fp64              0          0            %
> phase3-int8-matmul              0          0            %

I’m on x86-64 Gentoo with the latest gprbuild and gnatprove from alire.

It’s actually quite easy and cheap (about us$500).

And, of course, his AI could take him thru the steps :smiley: .

Its even easier to continually criticise and complain. Great Job.