Subject: Re: [bug#78016] [PATCH electronics-team] gnu: Add symbiyosys.

From: Maxim Cournoyer <[email-masked]>
Date: Fri, 25 Apr 2025 15:59:40 +0900

Hi,

Cayetano Santos <[email-masked]> writes:

> * gnu/packages/electronics.scm (symbiyosys): New variable.

Neat!

[...]

> +    (arguments
> +     (list
> +      #:test-target "test"
> +      #:make-flags #~(list (string-append "PREFIX=" #$output))
> +      #:phases #~(modify-phases %standard-phases
> +                   (delete 'configure)
> +                   (delete 'build)
> +                   ;; info: requires furo-ys, not yet available

I'd use: TODO: build docs, after furo-ys is packaged.

> +                   ;; (add-after 'install 'build-info
> +                   ;; (lambda _
> +                   ;; (invoke "make" "-C" "docs" "info")))
> +                   (add-before 'check 'create-git

nitpick: I'd name the phase to 'git-init or similar.

> +                     (lambda _
> +                       (invoke "git" "init"))) ;check expects a git repo
> +                   (add-after 'create-git 'patch-/usr/bin/env
> +                     (lambda _
> +                       (substitute* "sbysrc/sby_core.py"
> +                         (("\"/usr/bin/env\", ")
> +                          ""))
> +                       (substitute* "sbysrc/sby.py"
> +                         (("/usr/bin/env python")
> +                          (which "python3")))))

It looks like 'sby' is the test runner, so that should be OK, but just
to make sure: are these source used at runtime?  If so, `which` must not
be used to patch the source, as it picks things from the PATH at *build*
time, which in a cross-compilation setting would not point to the same
binaries.

For non-tests sources, the safe way is to find the file names or
commands via e.g. (search-input-file inputs "bin/python3") for example
(with the 'inputs' key exposed via the phase procedure).

> +                   ;; remove tests which fail

Please use complete sentences for standalone comments [0].  Also try to
explain the failures.  When they cannot be explained it's best to report
them to the upstream project and keep a reference to the opened issue so
that resolution can be tracked.

[0]  See (info "(standards) Comments") from the gnu-standards package.

> +                   (add-after 'patch-/usr/bin/env 'delete-check-failures

I'd name this phase 'disable-problematic-tests.  Note that if this uses
the Automake test harness (it seems it does not, using sby instead),
then setting the make variable (flag) XFAIL_TESTS with the
space-separated names of the failing tests could be a better way, see
(info "(automake) Parallel Test Harness").

> +                     (lambda _
> +                       (delete-file "tests/keepgoing/keepgoing_multi_step.sby")
> +                       (delete-file-recursively "docs/examples/demos")
> +                       (delete-file
> +                        "tests/regression/aim_vs_smt2_nonzero_start_offset.sby"))))))
> +    (inputs (list yosys abc))

Please list in lexicographical order.

> +    (native-inputs (list
> +                    ;; python-sphinx python-sphinx-argparse texinfo ; info

Maybe add a standalone

;; TODO: see above build-info phase comment.

instead of the '; info' margin comment.

nitpick: no need for a space between ';' and the margin comment.

> +                    python
> +                    python-click
> +                    python-xmlschema
> +                    git-minimal/pinned
> +                    boolector
> +                    yices
> +                    z3))

Again, please sort :-)

> +    (home-page "https://github.com/YosysHQ/sby/")
> +    (synopsis "Formal verification with yosys")

I'd say 'Formal hardware verification with yosys'

Other than that it looks good to me!  Could you please send a v2?

-- 
Thanks,
Maxim