Re: [Proposal] The Formal Methods in GNU Guix Working Group
Hi Ludo’, all, Thanks for your vote(s) of confidence, Ludo’; it’s great to hear! Ludovic Courtès writes: > Hi! > > Brett Gilio skribis: > >> 100% Agreed. Amin is also working on packaging the Lean prover and I am >> taking an interest in seeing if we can extend the OPAM importer to have >> a subimporter for Coq. > > That’d be nice! > I just sent in the very first patch inspired (in part) by this proposal to guix-patches: https://issues.guix.gnu.org/issue/38770 :-) > >> Ludo, what do you think about an https://fm.guix.gnu.org/ URL hosting a >> haunt webpage designed by Amin and I (and maybe others) to detail the >> purpose, goal, and maybe institutional use cases (research papers) of >> GNU Guix in the formal methods community? > > The domain name would have to be discussed with others (other > maintainers in particular; perhaps a better choice would be > formal-methods.guix.info or fm.guix.info, next to hpc.guix.info), but > the idea sounds great to me! > Sure! I’d love to hear from others (esp. other maintainers) about this. Personally, being a GNU maintainer, webmaster, and Savannah hacker, I’m (almost by definition :-)) partial to using *.gnu.org and various pieces of the GNU infra (lists, Savannah source repositories, …) for GNU work whenever possible. As such, I naturally like fm.guix.gnu.org better as the domain, and would prefer to use Savannah for hosting our sources, e.g. the Haunt sources for the Guix-FM site. What do you think? Like Brett, I’d be curious to hear the reasons for using *.guix.info and a non-Savannah repository forge for Guix-HPC. > > Thanks, > Ludo’. Best, amin signature.asc Description: PGP signature
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Ludovic Courtès writes: > For the record, I don’t work with the formal methods people at Inria, > but we chat occasionally, and I’d be happy to draw their attention to > this effort. :-) I thought not, but I think this smells of potential for collaboration maybe amongst a few there. I know some INRIA people from the Caml and Coq community, so I think if they see a notification both internally and externally of what is happening with this proposal (after we establish it a bit more) it has the potential to get some attention. > That’s sounds very ambitious, though it’s not like people here haven’t > been ambitious so far. ;-) It is absolutely an ambitious task, and is definitely a daunting one to try and make happen. I do have some experience with compiler construction, but nothing quite to this extent. Amin and I have been trying to establish connections with other people who might share this goal, and from what we've received it is _this_ particular task of making a bootstrapping compiler for ML that seems to be the most attention-getting. There is definitely a need here, we realized. So, if we are able to garner enough people to help make this task more manageable then I say it is in the realm of possibility and will prove useful for Guix. > Note that there’s an alternative tradition of theorem provers in Lisp > with ACL2, “The Little Prover”, etc. I am familiar :). The Little Prover and the Little Typer are foundational to my interest here. I have not considered ways to include them, so food for thought! > I agree with Julien that a separate IRC channel is unneeded at this > stage; as for the structure, I would start with a web page explaining > your areas of interests, similar to the Guix-HPC thing. > > To me, an important goal is to create ties with formal methods people, > and to increase the bandwidth between us. That can beget new ideas and > perspectives. > > Then there are specific areas where we should be discussing: compiler > bootstrapping (what can OCaml, GHC, SMLNJ, etc. developers do to make > their compilers bootstrappable?), package management (how to turn OPAM, > etc. into functional package managers, or how to get language X to use > Guix instead of rolling its own?), development facilities (‘guix > environment’, channels like Julien’s Coq channel), and so on. > > These things take time and we don’t necessarily have an idea what the > outcome should be, but it’s definitely worthwhile. Agreed! 100%. We have a lot of lateral connection making to do, and I will help foster that any way I can. By the sound of it, Amin has already been working with some of the Lean prover people on Zulip to see what is possible for attracting some attention there. I will do my part on this as well, and once we get an organizational page made for the working group at whatever address it exists at, I think we will be able to get some cross-pollination like we need. I definitely want to do this the "right way". Thank you Ludo for your help! -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Ludovic Courtès writes: > The domain name would have to be discussed with others (other > maintainers in particular; perhaps a better choice would be > formal-methods.guix.info or fm.guix.info, next to hpc.guix.info), but > the idea sounds great to me! That is, of course, reasonable that we should pass this along for a community decision among the maintainers. Though, I do wonder a bit about the HPC project in its decision to host its domain on *.guix.info and use the Gitlab instance instead of Savannah for developing the haunt page? I am making an assumption it is for historical reasons, rather than it being intentionally to distance itself from our relationship with the GNU project, but I would like to know the story behind this decision. I am personally not partial to either domain: fm.guix.info or fm.guix.gnu.org. I just wonder about how that original decision came about :). -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Ludovic Courtès writes: > Hi! > > Julien Lepiller skribis: > >> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of >> itself (using a bootstrapped bytecode interpreter written in C) to >> build itself. Fortunately this situation is being worked on by a phd >> student of Xavier Leroy (and nixOS user) :). >> >> The plan is to write a compiler in C or Scheme (it currently exists, >> but is written in OCaml) for "miniML" a small subset of the OCaml >> language. Then, there is already an interpreter in miniML able to >> interpret the OCaml compiler compiling itself. Once the miniML >> compiler is bootstrapped, we will have a path from C to OCaml :) > > Do you have pointers to this work? > > Hannes of MirageOS also mentioned it at the Reproducible Builds Summit. > It sounds exciting! > > Ludo’. > I am also interested in this. MirageOS has a long lineage of making sensible decisions in their development aside from just designing their unikernel. So i'd really like to see if this becomes a possible bridge from C or Scheme to a bootstrappable OCaml. For what I wonder, I think this is something a formal methods community in Guix would be able to contribute to so we see to it that GNU Guix has a good foundation for making OCaml properly bootstrappable. -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
Re: Happy Holidays!
Hello! Thanks for the kind words and happy holidays everyone! :-) Ludo’.
Re: Mumi service
Hi! Ricardo Wurmus skribis: > Ludovic Courtès writes: [...] >> However, the currently packaged snapshot crashes when trying to retrieve >> information about a bug: >> >> --8<---cut here---start->8--- >> $ /gnu/store/qw2c84gnwk3sgivh2i8x98xx5gx73vxl-mumi-0.0.0-5.8a57c87/bin/mumi >> GET /issue/22883 >> In mumi/web/server.scm: >> 38:9 23 (handler _ _ _) >> In mumi/web/controller.scm: >> 38:21 22 (render-with-error-handling _ _) >>104:21 21 (_) >> In mumi/web/view/html.scm: >>274:19 20 (issue-page #) >> In mumi/messages.scm: >>185:16 19 (patch-messages 22883) >> In debbugs/soap.scm: >>163:19 18 (soap-invoke* # #> get-bug-message-numbe…> …) >> 157:7 17 (soap-invoke _ _ . _) >> In sxml/simple.scm: >> 143:4 16 (xml->sxml _ #:namespaces _ #:declare-namespaces? _ >> #:trim-whitespace? _ …) >> 143:4 15 (loop # () #f _) >> 143:4 14 (loop # () #f _) >> 143:4 13 (loop # () #f _) >> 143:4 12 (loop # () #f _) >> 143:4 11 (loop # () #f _) >> 143:4 10 (loop # () #f _) >> In sxml/upstream/SSAX.scm: >> 1896:21 9 (_ # #f #> sxml/s…> …) >> In sxml/ssax/input-parse.scm: >>103:21 8 (next-token _ (#\< #\& #\return) _ _) >> In ice-9/suspendable-ports.scm: >>683:15 7 (read-delimited _ _ _) >>184:27 6 (fill-input # _ _) >> 72:4 5 (read-bytes # #vu8(10 32 98 121 32 >> 109 97 …) …) >> In unknown file: >>4 (port-read # #vu8(10 32 98 121 32 >> 109 97 …) …) >> In web/response.scm: >>254:22 3 (read! #vu8(10 32 98 121 32 109 97 105 108 46 109 101 115 115 >> 97 103 …) …) >> In ice-9/suspendable-ports.scm: >>284:18 2 (get-bytevector-n! # #vu8(10 >> 32 98 …) …) >> 72:4 1 (read-bytes # #vu8(10 32 98 >> 121 32 …) …) >> In unknown file: >>0 (port-read # #vu8(10 32 98 >> 121 32 …) …) >> In procedure custom_binary_input_port_read: Value out of range: 1024 >> --8<---cut here---end--->8--- >> >> Does that ring a bell, Ricardo? Should we update to a newer snapshot? > > This is exactly the same bug I hit when using mumi with (fibers web > server). With just the regular Guile (web server) it works fine but > seemingly leaks file handles until it is restarted. > > I don’t understand this. Could it be that the ‘read!’ procedure of the custom binary input port (CBIP) returned by ‘make-delimited-input-port’ in (web response) returns 1024 when ‘count’ is in fact lower than 1024, or something along these lines? I would try adding ‘pk’ calls there to display ‘count’ and the return value. If that is true, then maybe the underlying issue is that ‘get-bytevector-n!’ in (ice-9 suspendable-ports) can return a value greater than ‘count’, presumably in the ‘fill-directly’ case. Hmmm! Ludo’.
Re: Importers as independent packages?
Hi Martin, Martin Becze skribis: > I have been working on a recursive importer that uses semantic > versioning over on #38408. It relies on guile-semver. I'm not exactly > sure how to add guile-semver as a dependency to guix. But I'm also not > sure that I should. Importers will probably not be used by the majority > of end users so would it make sense to put the importers in their own > package? This would also nicely solve recursive-import-semver's problem > of being dependent on guile-semver. > > Also in the future it would be nice if the crate import could read from > a Cargo.toml directly (this will make importing things like alacritty > much easier since it is not crates.io), which would probably mean have > yet another dependency (guile-toml). What do you think about this Guix? Good question. In the end, ‘guix pull’ takes care of providing the right dependency: guile-gcrypt, guile-json, guile-git, etc. So here it would just be a matter of telling (guix self) that the importer modules depend on guile-semver in addition to the rest. (Likewise, configure.ac and Makefile.am may have to check whether guile-semver is available.) IOW, it seems that we’re already set up to handle such things, as in “guix pull” will do the right thing. If, in the future, we end up having too many dependencies for developer tools like importers, we might need to consider changing “guix pull” so that it no longer pulls them in by default. I think we’re not there yet, though. Thanks, Ludo’.
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Hi Brett, Brett Gilio skribis: > 1. Just as the bootstrappability and guix-hpc projects have their own > websites documenting their efforts, I think it would be nice to have > https://fm.guix.gnu.org/ which would host a Haunt-generated > website. This website would be hosted in the Savannah project structure > for GNU Guix. This would document who is active in the coordination and > oversight of this working group, and would express a clear and mutual > relationship with the GNU Guix / Guix System project. Like I wrote in another message, the only question will be the domain name, but other than that it sounds great. > 2. Perhaps we should adopt a particular tag for the Guix Debbugs > tracker, so as to be able to clearly delineate that this particular > patch or bug is in relation with the formal methods working > group. Maybe something like [FM]. I’d say let’s figure it out when it becomes an issue. :-) > 3. It was suggested that maybe a #guix-fm IRC channel might be useful, > but we have had a mixed bag of opinions on this. I personally think that > keeping everything together is the better solution, but I'd still like > to hear acceptance or criticism of this idea. Keeping everything on #guix for now sounds like the right thing to me. > 4. A lot of documenting working group milestones (Working on a Coq > sub-importer for OPAM, writing a bootstrapping compiler for SML97, > doing regular packaging duties for formal methods projects, > communicating upstream about distribution package quality, and perhaps > even trying to do formal methods work via synthesis in GNU Guile / GNU > Guix would be likely best expressed on the mailing list, and the > https://fm.guix.gnu.org/ website, but this likely rests in the hands of > the GNU Guix maintainers, of which I am not. > > 5. Additionally, maybe making an introductory post on the > https://guix.gnu.org/ blog about the preliminary goals of the working > group, after having our own subdomain established, would be a good way > to attract some attention to the project by distributing links to it on > HackerNews, Reddit, and Formal Methods/Functional Programming-related > mailing lists. Sounds like a great plan to me! Ludo’.
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Hi! Julien Lepiller skribis: > I'm afraid OCaml is not bootstrappable. It uses a bytecode version of > itself (using a bootstrapped bytecode interpreter written in C) to > build itself. Fortunately this situation is being worked on by a phd > student of Xavier Leroy (and nixOS user) :). > > The plan is to write a compiler in C or Scheme (it currently exists, > but is written in OCaml) for "miniML" a small subset of the OCaml > language. Then, there is already an interpreter in miniML able to > interpret the OCaml compiler compiling itself. Once the miniML > compiler is bootstrapped, we will have a path from C to OCaml :) Do you have pointers to this work? Hannes of MirageOS also mentioned it at the Reproducible Builds Summit. It sounds exciting! Ludo’.
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Hi! Brett Gilio skribis: > Having Guix and the Formal Methods community aligned would mean a great > deal of power for both camps! Just as we see with the Software Heritage > project and Guix, for providing historical and state-consistent > reproducible environments for software testing we and correspond to > formal methods much of the same guarantees of deterministic > computational states, modeling, and reasoning in software correctness. > > Amin, Leo, and I all likely agree that _some_ relationship here is good > to be opened and explored! I know that there are some of us who come > from institutions that have historical relationships to the proof > assistant community, Caml, HOL (looking at you Ludo', though IIRC you > are in a different working group at INRIA), > so this could be more of a chance to see bigger institutions begin to > adopt Guix for their research work. For the record, I don’t work with the formal methods people at Inria, but we chat occasionally, and I’d be happy to draw their attention to this effort. :-) > What follows is proposals for some of the work to be done by this > working group: > > -- A lot of proof assistants are based on dialects of ML. Most of these >use SMLnj or MLton for their work. To date there is an issue of >source-based bootstrapping of _all_ of the major ML compilers. We do >have PolyML in our repositories, but even this uses space-inefficient >text file blobs for compiling and is not a fully C-based source >bootstrap. Basically, all of the ML compilers rely on some distinct >pre-compiled something-or-other to get to their pristine state. I >have explored the idea, along with Leo and Amin, about following in >the tradition of MES (and mrustc) and starting an analogous GNU project for >writing a reduced-size specification ML bootstrapping compiler. That >way we can end the loop of a source-based build of ML97 compilers >being basically impossible. >[See issues #38605 & #38606 on DEBBUGS. Also, see >https://github.com/MLton/mlton/issues/350.] That’s sounds very ambitious, though it’s not like people here haven’t been ambitious so far. ;-) Note that there’s an alternative tradition of theorem provers in Lisp with ACL2, “The Little Prover”, etc. > -- Begin adding more projects that are important works in the formal >methods community. We have Coq, Idris, and Agda, but there is a lot of work >to be done on keeping these projects not only up-to-date but also >adding subprojects that use these toolchains. For example: C Minor, >Metamath, Ynot, Formally verified Featherweight Scala, RustBelt, >RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of >various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid >Haskell, extensions to Z3, and tons more! +1 > -- Possibly begin formally verifying some of the behavior and >implementations of GNU Guix and GNU Guile. This is kind of an add-on >idea, but it struck our interest so why leave it out? Put this way, it seems very broad. One thing I’d like to have is (1) Racket-style contracts, in particular for our record types, and (2) Turnstile-style static type checking, again primarily for record types. > -- Begin giving talks on the benefits of GNU Guix at conferences around >Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc. +1! > All of this seems really nice and impressive, but what is it without > getting some feedback from the community? I'd _really_ love to hear your > thoughts, experiences, and more on this working group idea and other > working groups to avoid pitfalls. Maybe we should have a secondary > #guix-fm channel on IRC? There is definitely a lot of work to be done > here, and we will need some form of organizational structure to keep the > work consistent and neatly integrated with the goals and purposes of GNU > Guix. I agree with Julien that a separate IRC channel is unneeded at this stage; as for the structure, I would start with a web page explaining your areas of interests, similar to the Guix-HPC thing. To me, an important goal is to create ties with formal methods people, and to increase the bandwidth between us. That can beget new ideas and perspectives. Then there are specific areas where we should be discussing: compiler bootstrapping (what can OCaml, GHC, SMLNJ, etc. developers do to make their compilers bootstrappable?), package management (how to turn OPAM, etc. into functional package managers, or how to get language X to use Guix instead of rolling its own?), development facilities (‘guix environment’, channels like Julien’s Coq channel), and so on. These things take time and we don’t necessarily have an idea what the outcome should be, but it’s definitely worthwhile. Thanks, Ludo’.
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Hi! Brett Gilio skribis: > 100% Agreed. Amin is also working on packaging the Lean prover and I am > taking an interest in seeing if we can extend the OPAM importer to have > a subimporter for Coq. That’d be nice! > Ludo, what do you think about an https://fm.guix.gnu.org/ URL hosting a > haunt webpage designed by Amin and I (and maybe others) to detail the > purpose, goal, and maybe institutional use cases (research papers) of > GNU Guix in the formal methods community? The domain name would have to be discussed with others (other maintainers in particular; perhaps a better choice would be formal-methods.guix.info or fm.guix.info, next to hpc.guix.info), but the idea sounds great to me! Thanks, Ludo’.
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Ludovic Courtès writes: > Hi! > > Julien Lepiller skribis: > >> I forgot to metion I have a small channel at >> https://framagit.org/tyreunom/guix-coq-channel that keeps track of >> every coq version since 8.6. I use it to test my coquille plugin on >> every coq version that exists, but I'm sure there are other use cases >> :) > > That’s an interesting kind of channel that’d be worth promoting (I think > many people have similar needs for their CI.) If you feel like writing > a blog post over the holidays… ;-) > > It’s also a very concrete item that’s directly useful to formal methods > people, a good way to create ties. 100% Agreed. Amin is also working on packaging the Lean prover and I am taking an interest in seeing if we can extend the OPAM importer to have a subimporter for Coq. Ludo, what do you think about an https://fm.guix.gnu.org/ URL hosting a haunt webpage designed by Amin and I (and maybe others) to detail the purpose, goal, and maybe institutional use cases (research papers) of GNU Guix in the formal methods community? -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
Re: Packaging Jami progress
Dnia 2019-12-27, o godz. 21:32:10 Gábor Boskovits napisał(a): > Hello Jan, > > Thanks for working on this. Jami is really painful to package :D > > You should look for packages with debug output. That is the way the > debugging symbol files are generated > for a package. Currently not too many packages define it, but from an > example you can easily find out how to > include that into the interesting package. You can find further > infomation here: > https://guix.gnu.org/manual/en/html_node/Installing-Debugging-Files.html > Tried adding some configure flags for enabling debugging, but it seems it's not the cause. But there's a comment, I guess Pierre left, showing a similar error: ;; TODO: We must wrap ring-client-gnome to force using the ;; `sqlite-with-column-metadata' package instead of `sqlite' or else it ;; fails with: ;; ;; /gnu/store/...-qtbase-5.11.2/lib/qt5/plugins/sqldrivers/libqsqlite.so: ;; undefined symbol: sqlite3_column_table_name16 ;; ;; qtbase is built against sqlite-with-column-metadata but somehow ;; jami-client-gnome ends up with both `sqlite' and ;; `sqlite-with-column-metadata' as inputs and it seems that ;; libqsqlite.so gets confused. I have no idea what does it means though. Could someone explain to me what needs to be done in *simple language* please? > > Best regards, > g_bor Jan Wielkiewicz
Re: bug#22883: Authenticating Git checkouts: step #1
Do I need to update anything on Savannah when I extend the expiration of my GPG key? On January 1st, I think my key will appear to expire unless the keyring was refreshed very recently. -- Alex Griffin On Fri, Dec 27, 2019, at 8:47 PM, Ricardo Wurmus wrote: > > Hi Ludo, > > > I’ve now committed this file: > > > > b3011dbbd2 doc: Mention "make authenticate". > > 787766ed1e git-authenticate: Keep a local cache of > > previously-authenticated commits. > > 785af04a75 git: 'commit-difference' takes a list of excluded commits. > > 1e43ab2c03 Add 'build-aux/git-authenticate.scm'. > > > > Commit 787766ed1e takes care of caching (one of the limitations I > > mentioned in my previous message). > > > > Commit b3011dbbd2 adds instructions for contributors on how to > > authenticate a checkout (copied below). It’s a bit bumpy so I would > > very much welcome feedback and suggestions on how to improve this! > > This is great! > > Thank you for the instructions. I thought I had all keys, but > apparently at least one of them is missing. “make authenticate” fails > for me with this error: > > Throw to key `srfi-34' with args `(# "could not authenticate commit > b291c9570d5a27b11472df3df61cef9ed012241b: key > B943509D633E80DD27FC4EED634A8DFFD3F631DF is missing"] 7f70fb08c240>)'. > > I previously downloaded the gpg keyring from Savannah: > > https://savannah.gnu.org/project/memberlist-gpgkeys.php?group=guix > > Looks like Hartmut used to use a different key, which I don’t have. > > -- > Ricardo > > >
Re: bug#22883: Authenticating Git checkouts: step #1
Hi Ludo, > I’ve now committed this file: > > b3011dbbd2 doc: Mention "make authenticate". > 787766ed1e git-authenticate: Keep a local cache of previously-authenticated > commits. > 785af04a75 git: 'commit-difference' takes a list of excluded commits. > 1e43ab2c03 Add 'build-aux/git-authenticate.scm'. > > Commit 787766ed1e takes care of caching (one of the limitations I > mentioned in my previous message). > > Commit b3011dbbd2 adds instructions for contributors on how to > authenticate a checkout (copied below). It’s a bit bumpy so I would > very much welcome feedback and suggestions on how to improve this! This is great! Thank you for the instructions. I thought I had all keys, but apparently at least one of them is missing. “make authenticate” fails for me with this error: Throw to key `srfi-34' with args `(#)'. I previously downloaded the gpg keyring from Savannah: https://savannah.gnu.org/project/memberlist-gpgkeys.php?group=guix Looks like Hartmut used to use a different key, which I don’t have. -- Ricardo
Re: Packaging Jami progress
Hello Jan, Thanks for working on this. Jan Wielkiewicz ezt írta (időpont: 2019. dec. 27., P, 20:11): > > Tested Jami with gnutls 3.6.10, but I get the same bug. I reported it > to Jami developers, but they can't reproduce the bug. > Here's more info, if anyone has any idea what could be the cause, then > please tell me: > https://git.jami.net/savoirfairelinux/ring-client-gnome/issues/1123 > > I need to find out what's wrong with our package. How do I debug > something on Guix System? I used "guix environment guix", then > "./pre-inst-env guix environment jami --ad-hoc gdb", then after running > gdb and passing the proper path to it and pressing "r", it displays the > following error: > > Reading symbols from > /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real... > (No debugging symbols found in > /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real) > (gdb) r Starting program: > /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real > [Thread debugging using libthread_db enabled] Using host libthread_db > library > "/gnu/store/ahqgl4h89xqj695lgqvsaf6zh2nhy4pj-glibc-2.29/lib/libthread_db.so.1". > [New Thread 0x7fffee145700 (LWP 4795)] [New Thread 0x7fffed944700 (LWP > 4796)] ** Message: 19:45:55.037: Jami GNOME client version: > 501cb99929f171ede62a96c675d51ffe0581ce5c ** Message: 19:45:55.038: git > ref: unknown [New Thread 0x7fffeca91700 (LWP 4797)] No migration > required > /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real: > symbol lookup error: > /gnu/store/371gzl7v7c8p0waasm4kwkalvgqmskav-qtbase-5.12.6/lib/qt5/plugins/sqldrivers/libqsqlite.so: > undefined symbol: sqlite3_column_table_name16 [Thread 0x7fffeca91700 > (LWP 4797) exited] [Thread 0x7fffed944700 (LWP 4796) exited] [Thread > 0x7fffee145700 (LWP 4795) exited] [Inferior 1 (process 4789) exited > with code 0177] (gdb) You should look for packages with debug output. That is the way the debugging symbol files are generated for a package. Currently not too many packages define it, but from an example you can easily find out how to include that into the interesting package. You can find further infomation here: https://guix.gnu.org/manual/en/html_node/Installing-Debugging-Files.html > > > Jan Wielkiewicz > Best regards, g_bor -- OpenPGP Key Fingerprint: 7988:3B9F:7D6A:4DBF:3719:0367:2506:A96C:CF63:0B21
Re: Packaging Jami progress
Tested Jami with gnutls 3.6.10, but I get the same bug. I reported it to Jami developers, but they can't reproduce the bug. Here's more info, if anyone has any idea what could be the cause, then please tell me: https://git.jami.net/savoirfairelinux/ring-client-gnome/issues/1123 I need to find out what's wrong with our package. How do I debug something on Guix System? I used "guix environment guix", then "./pre-inst-env guix environment jami --ad-hoc gdb", then after running gdb and passing the proper path to it and pressing "r", it displays the following error: Reading symbols from /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real... (No debugging symbols found in /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real) (gdb) r Starting program: /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real [Thread debugging using libthread_db enabled] Using host libthread_db library "/gnu/store/ahqgl4h89xqj695lgqvsaf6zh2nhy4pj-glibc-2.29/lib/libthread_db.so.1". [New Thread 0x7fffee145700 (LWP 4795)] [New Thread 0x7fffed944700 (LWP 4796)] ** Message: 19:45:55.037: Jami GNOME client version: 501cb99929f171ede62a96c675d51ffe0581ce5c ** Message: 19:45:55.038: git ref: unknown [New Thread 0x7fffeca91700 (LWP 4797)] No migration required /gnu/store/30jjbf7jkddw6z679c0h8zvifwaaakn0-jami-20191224.1.5c0154a/bin/.jami-gnome-real: symbol lookup error: /gnu/store/371gzl7v7c8p0waasm4kwkalvgqmskav-qtbase-5.12.6/lib/qt5/plugins/sqldrivers/libqsqlite.so: undefined symbol: sqlite3_column_table_name16 [Thread 0x7fffeca91700 (LWP 4797) exited] [Thread 0x7fffed944700 (LWP 4796) exited] [Thread 0x7fffee145700 (LWP 4795) exited] [Inferior 1 (process 4789) exited with code 0177] (gdb) Jan Wielkiewicz
Re: [Proposal] The Formal Methods in GNU Guix Working Group
Hi! Julien Lepiller skribis: > I forgot to metion I have a small channel at > https://framagit.org/tyreunom/guix-coq-channel that keeps track of > every coq version since 8.6. I use it to test my coquille plugin on > every coq version that exists, but I'm sure there are other use cases > :) That’s an interesting kind of channel that’d be worth promoting (I think many people have similar needs for their CI.) If you feel like writing a blog post over the holidays… ;-) It’s also a very concrete item that’s directly useful to formal methods people, a good way to create ties. Ludo’.
Re: bug#22883: Authenticating Git checkouts: step #1
Hello Guix! Ludovic Courtès skribis: > To begin with, I propose the attached script: when given a commit range, > it authenticates each commit, meaning that it ensures commits have a > valid signature and that that signature was made by one of the > authorized keys. Sample session: > > $ time ./pre-inst-env guile -e git-authenticate > build-aux/git-authenticate.scm d68de958b60426798ed62797ff7c96c327a672ac > 099ce5d4901706dc2c5be888a5c8cbf8fcd0d576 > Authenticating d68de95 to 099ce5d (7938 commits)... > Signing statistics: > BCA689B636553801C3C62150197A5888235FACAC 1454 > 3CE464558A84FDC69DB40CFB090B11993D9AEBB5 1025 > BBB02DDF2CEAF6A80D1DE643A2A06DF2A33A54FA941 > > [...] > > real 2m21.272s > user 1m38.741s > sys 0m59.546s I’ve now committed this file: b3011dbbd2 doc: Mention "make authenticate". 787766ed1e git-authenticate: Keep a local cache of previously-authenticated commits. 785af04a75 git: 'commit-difference' takes a list of excluded commits. 1e43ab2c03 Add 'build-aux/git-authenticate.scm'. Commit 787766ed1e takes care of caching (one of the limitations I mentioned in my previous message). Commit b3011dbbd2 adds instructions for contributors on how to authenticate a checkout (copied below). It’s a bit bumpy so I would very much welcome feedback and suggestions on how to improve this! Thanks in advance! Ludo’. --8<---cut here---start->8--- If you want to hack Guix itself, it is recommended to use the latest version from the Git repository: git clone https://git.savannah.gnu.org/git/guix.git How do you ensure that you obtained a genuine copy of the repository? Guix itself provides a tool to “authenticate” your checkout, but you must first make sure this tool is genuine in order to “bootstrap” the trust chain. To do that, run: git verify-commit `git log --format=%H build-aux/git-authenticate.scm` The output must look something like: gpg: Signature made Fri 27 Dec 2019 01:27:41 PM CET gpg:using RSA key 3CE464558A84FDC69DB40CFB090B11993D9AEBB5 ... gpg: Signature made Fri 27 Dec 2019 01:25:22 PM CET gpg:using RSA key 3CE464558A84FDC69DB40CFB090B11993D9AEBB5 ... ... meaning that changes to this file are all signed with key ‘3CE464558A84FDC69DB40CFB090B11993D9AEBB5’ (you may need to fetch this key from a key server, if you have not done it yet). From there on, you can authenticate all the commits included in your checkout by running: make authenticate The first run takes a couple of minutes, but subsequent runs are faster. Note: You are advised to run ‘make authenticate’ after every ‘git pull’ invocation. This ensures you keep receiving valid changes to the repository --8<---cut here---end--->8--- signature.asc Description: PGP signature
Re: TeX Live 2019 wanted
On Mon, Dec 16, 2019 at 11:41:57PM +0100, Marius Bakke wrote: > Errh, the patch only works if you already have Poppler 0.83.0. For the > current 'core-updates' branch, I believe you can use the same approach > but fetch poppler-0.76.0.cc instead (or take Arch's patch[0]). Ah, this is rocket science! I guessed so much as to use the 0.76.0 file; however, the build now fails with the following: /gnu/store/29jhbbg1hf557x8j53f9sxd9imlmf02a-bash-minimal-5.0.7/bin/bash ./libtool --tag=CXX --mode=link g++ -Wreturn-type -Wno-write-strings -g -O2 -o pdftex pdftexdir/pdftex-pdftexextra.o synctexdir/pdftex-synctex.o pdftex-pdftexini.o pdftex-pdftex0.o pdftex-pdftex-pool.o libpdftex.a -L/gnu/store/3snpwk7jl8i125bhiilvk9scqc4mnsx7-libpng-1.6.37/lib -L/gnu/store/qx7p7hiq90mi7r78hcr9cyskccy2j4bg-zlib-1.2.11/lib -lpng16 -lz -lz -L/gnu/store/18q4r8bpwmpm4w15zipf66l3bvdjzfbs-poppler-0.79.0/lib -lpoppler libmd5.a lib/lib.a /tmp/guix-build-texlive-bin-20190410.drv-0/build/texk/kpathsea/libkpathsea.la -lm libtool: link: g++ -Wreturn-type -Wno-write-strings -g -O2 -o pdftex pdftexdir/pdftex-pdftexextra.o synctexdir/pdftex-synctex.o pdftex-pdftexini.o pdftex-pdftex0.o pdftex-pdftex-pool.o libpdftex.a -L/gnu/store/3snpwk7jl8i125bhiilvk9scqc4mnsx7-libpng-1.6.37/lib -L/gnu/store/qx7p7hiq90mi7r78hcr9cyskccy2j4bg-zlib-1.2.11/lib /gnu/store/3snpwk7jl8i125bhiilvk9scqc4mnsx7-libpng-1.6.37/lib/libpng16.so -lz -L/gnu/store/18q4r8bpwmpm4w15zipf66l3bvdjzfbs-poppler-0.79.0/lib -lpoppler libmd5.a lib/lib.a /tmp/guix-build-texlive-bin-20190410.drv-0/build/texk/kpathsea/.libs/libkpathsea.a -lm -Wl,-rpath -Wl,/gnu/store/3snpwk7jl8i125bhiilvk9scqc4mnsx7-libpng-1.6.37/lib -Wl,-rpath -Wl,/gnu/store/3snpwk7jl8i125bhiilvk9scqc4mnsx7-libpng-1.6.37/lib ld: libpdftex.a(libpdftex_a-writeimg.o): in function `readimage': /tmp/guix-build-texlive-bin-20190410.drv-0/build/texk/web2c/../../../texlive-20190410-source/texk/web2c/pdftexdir/writeimg.c:320: undefined reference to `read_pdf_info' ld: libpdftex.a(libpdftex_a-writeimg.o): in function `undumpimagemeta': /tmp/guix-build-texlive-bin-20190410.drv-0/build/texk/web2c/../../../texlive-20190410-source/texk/web2c/pdftexdir/writeimg.c:546: undefined reference to `read_pdf_info' collect2: error: ld returned 1 exit status read_pdf_info is defined precisely in the pdftoepdf-poppler*.cc And using "strings" on libpdftex.a shows that the function name occurs. Andreas
