Search Results: "abe"

22 November 2017

Daniel Pocock: VR Hackathon at FIXME, Lausanne (1-3 December 2017)

The FIXME hackerspace in Lausanne, Switzerland is preparing a VR Hackathon on the weekend of 1-3 December. Competitors and visitors are welcome, please register here. Some of the free software technologies in use include Blender and Mozilla VR.

15 November 2017

Steinar H. Gunderson: Introducing Narabu, part 6: Performance

Narabu is a new intraframe video codec. You probably want to read part 1, part 2, part 3, part 4 and part 5 first. Like I wrote in part 5, there basically isn't a big splashy ending where everything is resolved here; you're basically getting some graphs with some open questions and some interesting observations. First of all, though, I'll need to make a correction: In the last part, I wrote that encoding takes 1.2 ms for 720p luma-only on my GTX 950, which isn't correct I remembered the wrong number. The right number is 2.3 ms, which I guess explains even more why I don't think it's acceptable at the current stage. (I'm also pretty sure it's possible to rearchitect the encoder so that it's much better, but I am moving on to other video-related things for the time being.) I encoded a picture straight off my DSLR (luma-only) at various resolutions, keeping the aspect. Then I decoded it a bunch of times on my GTX 950 (low-end last-generation NVIDIA) and on my HD 4400 (ultraportable Haswell laptop) and measured the times. They're normalized for megapixels per second decoded; remember that doubling width (x axis) means quadruple the pixels. Here it is: Narabu decoding performance graph I'm not going to comment much beyond two observations: Encoding only contains the GTX 950 because I didn't finish the work to get that single int64 divide off: Narabu encoding performance graph This is interesting. I have few explanations. Probably more benchmarking and profiling would be needed to make sense of any of it. In fact, it's so strange that I would suspect a bug, but it does indeed seem to create a valid bitstream that is decoded by the decoder. Do note, however, that seemingly even on the smallest resolutions, there's a 1.7 ms base cost (you can't see it on the picture, but you'd see it in an unnormalized graph). I don't have a very good explanation for this either (even though there are some costs that are dependent on the alphabet size instead of the number of pixels), but figuring it out would probably be a great start for getting the performance up. So that concludes the series, on a cliffhanger. :-) Even though it's not in a situation where you can just take it and put it into something useful, I hope it was an interesting introduction to the GPU! And in the meantime, I've released version 1.6.3 of Nageru, my live video mixer (also heavily GPU-based) with various small adjustments and bug fixes found before and during Tr ndisk. And Movit is getting compute shaders for that extra speed boost, although parts of it is bending my head. Exciting times in GPU land :-)

Daniel Pocock: Linking hackerspaces with OpenDHT and Ring

Francois and Nemen at the FIXME hackerspace (Lausanne) weekly meeting are experimenting with the Ring peer-to-peer softphone: Francois is using Raspberry Pi and PiCam to develop a telepresence network for hackerspaces (the big screens in the middle of the photo). The original version of the telepresence solution is using WebRTC. Ring's OpenDHT potentially offers more privacy and resilience.

10 November 2017

Thadeu Lima de Souza Cascardo: Software Freedom Strategy with Community Projects

It's been some time since I last wrote. Life and work have been busy. At the same time, the world has been busy, and as I would love to write a larger post, I will try to be short here. I would love to touch on the Librem 5 and postmarketOS. In fact, I had, in a podcast in Portuguese, Papo Livre. Maybe, I'll touch a little on the latter. Some of the inspiration for this post include: All of those led me to understand how software freedom is under attack, in particular how copyleft in under attack. And, as I talked during FISL, though many might say that "Open Source has won", end users software freedom has not. Lots of companies have co-opted "free software" but give no software freedom to their users. They seem friends with free software, and they are. Because they want software to be free. But freedom should not be a value for software itself, it needs to be a value for people, not only companies or people who are labeled software developers, but all people. That's why I want to stop talking about free software, and talk more about software freedom. Because I believe the latter is more clear about what we are talking about. I don't mind that we use whatever label, as long as we stablish its meaning during conversations, and set the tone to distinguish them. The thing is: free software does not software freedom make. Not by itself. As Bradley Kuhn puts it: it's not magic pixie dust. Those who have known me for years might remember me as a person who studied free software licenses and how I valued copyleft, the GPL specifically, and how I concerned myself with topics like license compatibility and other licensing matters. Others might remember me as a person who valued a lot about upstreaming code. Not carrying changes to software openly developed that you had not made an effort to put upstream. I can't say I was wrong on both accounts. I still believe in those things. I still believe in the importance of copyleft and the GPL. I still value sharing your code in the commons by going upstream. But I was certaily wrong in valuing them too much. Or not giving as much or even more value to distribution efforts of getting software freedom to the users. And it took me a while in seeing how many people also saw the GPL as a tool to get code upstream. You see that a lot in Linus' discourse about the GPL. And that is on the minds of a lot of people, who I have seen argue that copyleft is not necessary for companies to contribute code back. But that's the problem. The point is not about getting code upstream. But about assuring people have the freedom to run a modified version of the software they received on their computers. It turns out that many examples of companies who had contributed code upstream, have not delivered that freedom to their end-users, who had received a modified version of that same software, which is not free. Bradley Kuhn also alerts us that many companies have been replacing copyleft software with non-copyleft software. And I completely agree with him that we should be writing more copyleft software that we hold copyright for, so we can enforce it. But looking at what has been happening recently in the Linux community about enforcement, even thought I still believe in enforcement as an strategy, I think we need much more than that. And one of those strategies is delivering more free software that users may be able to install on their own computers. It's building those replacements for software that people have been using for any reason. Be it the OS they get when they buy a device, or the application they use for communication. It's not like the community is not doing it, it's just that we need to acknowledge that this is a necessary strategy to guarantee software freedom. That distribution of software that users may easily install on their computers is as much or even more valuable than developing software closer to the hacker/developer community. That doing downstream changes to free software in the effort of getting them to users is worth it. That maintaining that software stable and secure for users is a very important task. I may be biased when talking about that, as I have been shifting from doing upstream work to downstream work and both on the recent years. But maybe that's what I needed to realize that upstreaming does not necessarily guarantees that users will get software freedom. I believe we need to talk more about that. I have seen many people dear to me disregard that difference between the freedom of the user and the freedom of software. There is much more to talk about that, go into detail about some of those points, and I think we need to debate more. I am subscribed to the libreplanet-discuss mailing list. Come join us in discussing about software freedom there, if you want to comment on anything I brought up here. As I promised I would, I would like to mention about postmarketOS, which is an option users have now to get some software freedom on some mobile devices. It's an effort I wanted to build myself, and I applaud the community that has developed around it and has been moving forward so quickly. And it's a good example of a balance between upstream and dowstream code that gets to deliver a better level of software freedom to users than the vendor ever would. I wanted to write about much of the topics I brought up today, but postponed that for some time. I was motivated by recent events in the community, and I am really disappointed at some the free software players and some of the events that happened in the last few years. That got me into thinking in how we need to manifest ourselves about those issues, so people know how we feel. So here it is: I am disappointed at how the Linux Foundation handled the situation about Software Freedom Conversancy taking a case against VMWare; I am disappointed about how Software Freedom Law Center handled a trademark issue against the Software Freedom Conservancy; and I really appreciate all the work the Software Freedom Conservancy has been doing. I have supported them for the last two years, and I urge you to become a supporter too.

06 November 2017

Jonathan Dowland: Coil

Peter Christopherson and Jhonn Balance, from [Santa Sangre](https://santasangremagazine.wordpress.com/2014/11/16/the-angelic-conversation-in-remembrance-of-coil/) Peter Christopherson and Jhonn Balance, from Santa Sangre
A friend asked me to suggest five tracks by Coil that gave an introduction to their work. Trying to summarize Coil in 5 tracks is tough. I think it's probably impossible to fairly summarize Coil with any subset of their music, for two reasons. Firstly, their music was the output of their work but I don't think is really the whole of the work itself. There's a real mystique around them. They were deeply interested in arcania, old magic, Aleister Crowley, scatology; they were both openly and happily gay and their work sometimes explored their experiences in various related underground scenes and sub-cultures; they lost friends to HIV/AIDS and that had a profound impact on them. They had a big influence on some people who discovered them who were exploring their own sexualities at the time and might have felt excluded from mainstream society. They frequently explored drugs, meditation and other ways to try to expand and open their minds; occultism. They were also fiercely anti-commercial, their stuff was released in limited quantities across a multitude of different music labels, often under different names, and often paired with odd physical objects, runes, vials of blood, etc. Later fascinations included paganism and moon worship. I read somewhere that they literally cursed one of their albums. Secondly, part of their "signature" was the lack of any consistency in their work, or to put it another way, their style over time varied enormously. I'm also not necessarily well-versed in all their stuff, I'm part way on this journey myself... but these are tracks which stand out at least from the subset I've listened to. Both original/core members of Coil have passed away and the legal status of their catalogue is in a state of limbo. Some of these songs are available on currently-in-print releases, but all such releases are under dispute by some associate or other.

1. Heaven's Blade Like (probably) a lot of Coil songs, this one exists in multiple forms, with some dispute about which are canonical, which are officially sanctioned, etc. the video linked above actually contains 5 different versions, but I've linked to a time offset to the 4th: "Heaven's Blade (Backwards)". This version was the last to come to light with the recent release of "Backwards", an album originally prepared in the 90s at Trent Reznor's Nothing Studios in New Orleans, but not finished or released. The circumstances around its present-day release, as well as who did what to it and what manipulation may have been performed to the audio a long time after the two core members had passed, is a current topic in fan circles. Despite that, this is my preferred version. You can choose to investigate the others, or not, at your own discretion.

2. how to destroy angels (ritual music for the accumulation of male sexual energy) A few years ago, "guidopaparazzi", a user at the Echoing the Sound music message board attempted to listen to every Coil release ever made and document the process. He didn't do it chronologically, leaving the EPs until near the end, which is when he tackled this one (which was the first release by Coil, and was the inspiration behind the naming of Trent Reznor's one-time side project "How To Destroy Angels"). Guido seemed to think this was some kind of elaborate joke. Personally I think it's a serious piece and there's something to it but this just goes to show, different people can take things in entirely different ways. Here's Guido's review, and you can find the rest of his reviews linked from that one if you wish. https://archive.org/details/Coil-HowToDestroyAngels1984

3. Red Birds Will Fly Out Of The East And Destroy Paris In A Night Both "Musick To Play In The Dark" volumes (one and two) are generally regarded as amongst the most accessible entry points to the Coil discography. This is my choice of cut from volume 1. For some reason this reminds me a little of some of the background music from the game "Unreal Tournament". I haven't played that in at least 15 years. I should go back and see if I can figure out why it does. The whole EP is worth a listen, especially at night. https://archive.org/details/CoilMusickToPlayInTheDarkVol1/Coil+-+Musick+To+Play+In+The+Dark+Vol+1+-+2+Red+Birds+Will+Fly+Out+Of+The+East+And+Destroy+Paris+In+A+Night.flac

4. Things Happen It's tricky to pick a track from either "Love's Secret Domain" or "Horse Rotorvator"; there are other choices which I think are better known and loved than this one but it's one that haunted me after I first heard it for one reason or another, so here it is.

5. The Anal Staircase Track 1 from Horse Rotorvator. What the heck is a Horse Rotorvator anyway? I think it was supposed to have been a lucid nightmare experienced by the vocalist Jhonn Balance. So here they wrote a song about anal sex. No messing about, no allusion particularly, but why should there be? https://archive.org/details/CoilHorseRotorvator2001Remaster/Coil+-+Horse+Rotorvator+%5B2001+remaster%5D+-+01+The+Anal+Staircase.flac

Bonus 6th: 7-Methoxy-B-Carboline (Telepathine) From the drone album "Time Machines", which has just been re-issued by DIAS records, who describe it as "authorized". Each track is titled by the specific combination of compounds that inspired its composition, supposedly. Or, perhaps it's a "recommended dosing" for listening along. https://archive.org/details/TimeMachines-TimeMachines

Post-script If those piqued your interest, there's some decent words and a list of album suggestions in this Vinyl Factory article. Finally, if you can track them down, Stuart Maconie had two radio shows about Coil on his "Freak Zone" programme. The main show discusses the release of "Backwards", including an interview with collaborator Danny Hyde, who was the main person behind the recent re-issue. The shorter show is entitled John Doran uncoils Coil. Guest John Doran from The Quietus discusses the group and their history interspersed with Coil tracks and tracks from their contemporaries. Interestingly they chose a completely different set of 5 tracks to me.

31 October 2017

Chris Lamb: Free software activities in October 2017

Here is my monthly update covering what I have been doing in the free software world in October 2017 (previous month):
Reproducible builds

Whilst anyone can inspect the source code of free software for malicious flaws, most software is distributed pre-compiled to end users. The motivation behind the Reproducible Builds effort is to allow verification that no flaws have been introduced either maliciously or accidentally during this compilation process by promising identical results are always generated from a given source, thus allowing multiple third-parties to come to a consensus on whether a build was compromised. I have generously been awarded a grant from the Core Infrastructure Initiative to fund my work in this area. This month I:


I also made the following changes to our tooling:
diffoscope

diffoscope is our in-depth and content-aware diff utility that can locate and diagnose reproducibility issues.

  • Improve names in output of "internal" binwalk members. (#877525).
  • Don't crash on malformed md5sums files. (#877473).
  • Omit misleading "any of" prefix when only complaining about a single module on import. [...]
  • Adjust tests as ps2ascii now varies its output on timezone. [...]

strip-nondeterminism

strip-nondeterminism is our tool to remove specific non-deterministic results from a completed build.

  • Clojure considers .class file to be stale if it shares the same timestamp of the .clj. We thus adjust the timestamps of the .clj to always be younger. (#877418).
  • Print a message in --verbose mode if no canonical time was specified. [...]

buildinfo.debian.net

buildinfo.debian.net is my experiment into how to process, store and distribute .buildinfo files after the Debian archive software has processed them.

  • Always show SHA-256 checksums, regardless of the browser viewport size. [...]
  • Add an API endpoint to fetch specific .buildinfo files for a certain package/version/architecture. [...]


Debian My activities as the current Debian Project Leader are covered in my "Bits from the DPL" email to the debian-devel-announce mailing list.
Patches contributed
  • devscripts: Please print the actual arguments debuild makes to Lintian. (#880124)
  • hw-detect: Drop reference to floppy disks; it's almost 2018. (#880122)
  • debci:
    • Use deb.debian.org over http.debian.net. (#879654)
    • Document how to use an alternative mirror. (#879655)

Debian LTS

This month I have been paid to work 18 hours on Debian Long Term Support (LTS). In that time I did the following:
  • "Frontdesk" duties, triaging CVEs, etc.
  • Followed up on a large number of upstream "pings" that have been left dormant.
  • Issued DLA 1121-1 to fix an out-of-bounds read vulnerability in curl where a malicious FTP server could abuse this to prevent clients from interacting with it.
  • Issued DLA 1123-1 for the "Go" programming language where an attacker could generate a MIME request such that the server ran out of file descriptors.
  • Issued DLA 1126-1 for the libxfont font selection and rasterisation library, correcting two vulnerabilities, both involving the library being tricked into reading invalid/random memory.
  • Issued DLA 1134-1 for sdl-image1.2, an image loading library. A maliciously-crafted .xcf file could cause a stack-based buffer overflow resulting in potential code execution.

Uploads
  • python-django:
    • 2.0~beta1-1 New upstream 2.x release.
    • 1.11.6-1 New upstream bugfix release.
  • gunicorn (19.6.0-10+deb9u1) Prepared a release for stable to avoid a runtime dependency on a compiler. (#877722)
  • redis:
    • 4:4.0.2-3:
      • Drop the Debian-specific /etc/redis/redis-server.pre-up.d (etc.) hooks and remove them if unchanged.
      • Include systemd redis-server@.service and redis-sentinel@.service template files to easily run multiple Redis instances. (#877702)
      • Patch redis.conf and sentinel.conf with quilt instead of maintaining our own versions under debian/.
    • 4:4.0.2-4:
      • Add input validity checking to cluster config slot numbers to fix CVE-2017-15047. (#878076)
      • Drop debian/bin/generate-parts now we aren't calling it.
      • Correct Bash-ism in NEWS file.
    • 4:4.0.2-5: Replace the existing patch for CVE-2017-15047 with an upstream-blessed version that covers another case.
  • redisearch (0.21.3-5) Initial release.
  • docbook2man (2.0.0-40) Correct spelling mistakes in binaries and other misc packaging tidying.
  • python-redis (2.10.6-1) New upstream release.
  • bfs (1.1.3-1) New upstream release.

FTP Team

As a Debian FTP assistant I ACCEPTed 103 packages: amcheck, argagg, binutils, blockui, bro-pkg, chkservice, citus, django-axes, docker-containerd, doctest, dtkwidget, duktape, feed2exec, fontforge, fonttools, gcc-8, gcc-8-cross, generator-scripting-language, gitgraph.js, haskell-uri-encode, hoel, iniparser, its, jquery-areyousure, kodi, libcatmandu-mods-perl, libcatmandu-template-perl, libcatmandu-xml-perl, libcatmandu-xsd-perl, libcode-tidyall-plugin-sortlines-naturally-perl, libgdamm5.0, libinfinity, libmods-record-perl, libreoffice-dictionaries, libset-intervaltree-perl, libsodium, linux, linux-grsec, ltsp-manager, lxqt-themes, mailman3-core, measurement-kit, mini-buildd, musescore, node-babel, node-babel-eslint, node-babel-loader, node-babel-plugin-add-module-exports, node-babel-plugin-transform-define, node-gulp-newer, node-regenerate-unicode-properties, node-regexpu-core, node-regjsparser, node-unicode-data, node-unicode-loose-match, openjdk-9, orafce, pgaudit, pgsql-ogr-fdw, pk4, postgresql-mysql-fdw, powa-archivist, python-azure-devtools, python-colormap, python-darkslide, python-dotenv, python-karborclient, python-logfury, python-lupa, python-marshmallow, python-murano-pkg-check, python-octaviaclient, python-pathspec, python-pgpy, python-pydub, python-randomize, python-sabyenc, python-searchlightclient, python-stestr, python-subunit2sql, python-twitter, python-utils, python-wsgilog, r-cran-bindr, r-cran-desc, r-cran-hms, r-cran-readstata13, r-cran-rprojroot, r-cran-wikidatar, r-cran-wikipedir, r-cran-wikitaxa, repmgr, requests-file, resteasy3.0, sdl-kitchensink, stardicter, systemd-el, thunderbird, tomcat8.0, uwsgi-plugin-luajit, uwsgi-plugin-mongo, uwsgi-plugin-php & uwsgi-plugin-v8. I additionally filed 3 RC bugs against packages that had incomplete debian/copyright files against: fonttools, generator-scripting-language & libsodium.

Norbert Preining: Debian/TeX Live 2017.20171031-1

Halloween is here, time to upload a new set of scary packages of TeX Live. About a month has passed, so there is the usual big stream up updates. There was actually an intermediate release to get out some urgent fixes, but I never reported the news here. So here are the accumulated changes and updates. My favorite this time is wallcalendar, a great class to design all kind of calendars, it looks really well done. I immediately will start putting one together. On the font side there is the new addition coelacanth. To quote from the README: Coelacanth is inspired by the classic Centaur type design of Bruce Rogers, described by some as the most beautiful typeface ever designed. It aims to be a professional quality type family for general book typesetting. And indeed it is beautiful! Other noteworthy addition is the Spark font that allows creating sparklines in the running text with LaTeX. Enjoy. New packages algobox, amscls-doc, beilstein, bib2gls, coelacanth, crossreftools, dejavu-otf, dijkstra, ducksay, dynkin-diagrams, eqnnumwarn, fetchcls, fixjfm, glossaries-finnish, hagenberg-thesis, hecthese, ifxptex, isopt, istgame, ku-template, limecv, mensa-tex, musicography, na-position, notestex, outlining, pdfreview, spark-otf, spark-otf-fonts, theatre, unitn-bimrep, upzhkinsoku, wallcalendar, xltabular. Updated packages acmart, amsmath, animate, arabluatex, arara, babel, babel-french, bangorexam, baskervillef, beebe, biblatex-philosophy, biblatex-source-division, bibletext, bidi, bxjaprnind, bxjscls, bxpapersize, bytefield, classicthesis, cochineal, complexity, cooking-units, curves, datetime2-german, dccpaper, doclicense, docsurvey, eledmac, epstopdf, eqparbox, esami, etoc, fbb, fei, fithesis, fmtcount, fnspe, fonts-tlwg, fontspec, genealogytree, glossaries, glossaries-extra, hecthese, hepthesis, hvfloat, ifplatform, ifptex, inconsolata, jfmutil, jsclasses, ketcindy, knowledge, koma-script, l3build, l3experimental, l3kernel, l3packages, langsci, latex2man, latexbug, lato, leadsheets, libertinust1math, listofitems, luatexja, luatexko, luatodonotes, lwarp, markdown, mcf2graph, media9, newtx, novel, numspell, ocgx2, overpic, philokalia, phonenumbers, platex, poemscol, pst-exa, pst-geometrictools, pst-ovl, pst-plot, pst-pulley, pst-tools, pst-vehicle, pst2pdf, pstool, pstricks, pstricks-add, pxchfon, pxjahyper, quran, randomlist, rec-thy, reledmac, robustindex, scratch, skrapport, spectralsequences, tcolorbox, tetex, tex4ht, texcount, texdoc, tikzducks, tikzsymbols, toptesi, translation-biblatex-de, unicode-math, updmap-map, uplatex, widetable, xcharter, xepersian, xetexko, xetexref, xsim, zhlipsum.

29 October 2017

Russ Allbery: Review: Why We Sleep

Review: Why We Sleep, by Matthew Walker
Publisher: Scribner
Copyright: October 2017
ISBN: 1-5011-4433-2
Format: Kindle
Pages: 341
The world is full of theories, and corresponding books, about things that will make you healthier or prevent disease. Nearly all of them are scams, either intentional or created through the placebo effect and the human tendency to see patterns that don't exist. The rare ones that aren't have a certain pattern: they're grounded in our best understanding of biology, align with what our body wants to do anyway, have been thoroughly studied using proper testing methodology, and don't make money for powerful corporations. I'm fairly sure this is one of those rare ones that isn't a scam. And, if so, it's rather important and worth your attention. Matthew Walker is a professor of neuroscience and biology at the University of California at Berkeley, where he's the founder of the Center for Human Sleep Science. He's not a doctor; he started medical training, but (as he says in the book) found himself more attracted to questions than answers. He's a professional academic researcher who has been studying sleep for decades. This book is a combination of summary of the current state of knowledge of academic sleep research and a plea: get more sleep, because we're literally killing ourselves with the lack of it. Walker opens the book with a discussion of the mechanisms of sleep: how we biologically fall asleep and why, how this has changed over time, and how it changes with age. Along with that, he defines sleep: the REM and NREM sleep cycle that you may have already heard of, how it manifests itself in most people, and where dreams fit in. The second part then discusses what happens when you sleep, with a focus on what goes wrong when you don't. (Spoiler: A lot. Study after study, all cited and footnoted, has found connections between sleep and just about every aspect of mental and physical health.) The third part does the same for dreams, fitting them into the picture along with a scientific discussion of just what's going on during dreams. The fourth and final part tackles the problem: why don't we get enough sleep, and what can we do about it? I will warn in advance that this book will make you paranoid about your sleeping patterns. Walker has the missionary zeal of an academic who has sunk his teeth into something really important that society needs to take into account and will try to drown you in data, analysis, analogies, and sheer earnestness until you will believe him. He wants you to get at least seven, and preferably eight, hours of sleep a night. Every night, with as little variation as you can manage. Everyone, even if you think you're someone who doesn't need as much sleep (you're probably not). There's a ton of science here, a great popularization of a whole field of research, but this is also a book that's trying to get you to do something. Normally, that sort of book raises my shields. I'm not much of a believer in any book of the general genre of "most people are doing this basic part of life wrong, and should do it my way instead." But the hallmarks of good science are here: very widespread medical consensus, no corporate interest or obvious path to profit, and lots of studies (footnoted here, with some discussions of methodology although not the statistical details, which will require looking up the underlying studies and careful caveats where studies indicate correlation but may not find causes). And Walker makes the very telling point early in the book that nearly every form of life on the planet sleeps in one way or another (defined as a daily recurring period of time during which it doesn't respond to outside stimulus), which is a strong indicator of universal necessity. Given the vulnerability and loss of useful hours that come with sleep, one would expect some species to find an evolutionary path away from it if it were dispensable. But except for extremely short-lived species, we've never found a living creature that didn't sleep. Walker's argument for duration is also backed up by repeated studies on human capability before and after various quantities of sleep, and on studies of the sleep phases in various parts of the night. Study after study used six hours as the cutoff point and showed substantial deterioration in physical and mental capabilities even after only one night of short sleeping. (Reducing sleep to four hours is nearly catastrophic.) And, more worrisomely, that degradation is still measurable after "catching up" on sleep on subsequent nights. Sleeping in on weekends doesn't appear to fully compensate for the damage done by short-sleeping during the week. When Walker gets into the biological reasons for sleep, one starts to understand why it's so important. I think the part I found the most fascinating was the detailed analysis of what the brain is doing while you sleep. It's not inactive at all, even outside of REM sleep. Walker and other sleep researchers have done intriguing experiments showing how different parts of the sleep cycle transfer memories from short to long term storage, transfer physical skills into subconscious parts of the brain, discard short term memories that the conscious brain has tagged as being unwanted, and free up space for new knowledge acquisition. REM sleep appears to attempt to connect otherwise unrelated memories and bits of knowledge, inverting how association normally works in the brain, thus providing some concrete explanation for sleep's role in creativity. And (this research is fairly new), deep NREM sleep causes temporary physical changes in the brain that appear to be involved in flushing metabolic waste products away, including the plaque involved in Alzheimer's. The last part of the book is probably the most concretely useful: what can one practically do to get more sleep? There is quite a lot that's proven effective, but Walker starts with something else: sleeping pills. Here, you can almost see the lines drawn by a lawyer around what Walker should say. He stresses that he's not a medical doctor while laying out study after study that all point in the same direction: sleeping pills are a highly dangerous medical fraud that will shorten your lifespan for negligible benefit in helping you fall asleep, while limiting your brain's ability to enter true sleep. They're sedation, sedation is not sleep, and the four billion dollar sleeping pill market is literally making everything worse. The good news is there is an effective treatment for insomnia that works for many people; the better news is that it's completely free (although Walker does suggest some degree of medical supervision for serious insomnia so that some parts of it can be tailored to you). He walks through CBT-I (cognitive behavior therapy for insomnia), which is now the medically recommended primary treatment for insomnia, and takes apart the pieces to show how they line up with the results of sleep research studies. Alongside that are recommendations for improving sleep for people who don't have clinical insomnia but who aren't regularly getting the recommended amount of sleep. There are a lot of interesting bits here (and he of course talks about blue LED light and its relationship to melatonin cycles), but I think the most interesting for me was that you have to lower your core body temperature by a couple of degrees (Fahrenheit) to enter sleep. The temperature of your sleeping environment is therefore doubly important: temperature changes are one of the signals your body uses to regulate circadian rhythms (cold being a signal of night), and a colder sleeping area helps you lower your core body temperature so that you can fall asleep. (The average person does best with a sleeping room temperature of 65F, 18C.) There's even more in here: I haven't touched on Walker's attack on the US tendency to push high school start times earlier and earlier in the day (particularly devastating for teenagers, whose circadian rhythms move two hours later in the day than adults before slowly returning to an adult cycle). Or the serious problems of waking to an alarm clock, and the important benefits of the sleep that comes at the end of a full night's cycle. Or the benefits of dreams in dealing with trauma and some theories for how PTSD may interfere with that process. Or the effect of sleep on the immune system. Walker's writing style throughout Why We Sleep is engaging and clear, although sometimes too earnest. He really wants the reader to believe him and to get more sleep, and sometimes that leaks around the edges. One can also see the effort he's putting into not reading too much into research studies, but if there's a flaw in the science here, it's that I think Walker takes a few tentative conclusions a bit too far. (I'm sure these studies have the standard research problem of being frequently done on readily-available grad students rather than representative samples of the population, although the universality of sleep works in science's favor here.) Some of the recitations of research studies can get rather dry, and I once again discovered how boring I find most discussion of dreams, but for a first book written by an academic, this is quite readable. This is one of those books that I want everyone to read mostly so that they can get the information in it, not as much for the enjoyment of reading the book itself. I've been paying closer attention to my own sleep patterns for the last few years, and my personal experience lines up neatly with the book in both techniques to get better sleep and the benefits of that sleep. I'd already reached the point where I was cringing when people talk about regularly going on four or five hours of sleep; this is an entire book full of researched reasons to not do that. (Walker points out that both Reagan and Thatcher, who bragged about not requiring much sleep, developed Alzheimer's, and calls out Trump for making the same brag.) The whole book may not be of interest to everyone, but I think everyone should at least understand why the World Heath Organization recommends eight hours a night and labels shift work a probable carcinogen. And, as Walker points out, we should be teaching some of this stuff in school health classes alongside nutrition and sex education. Alas, Walker can't provide much advice on what I think is the largest robber of sleep: the constant time pressure of modern life, in which an uninterrupted nine hour sleep opportunity feels like an unaffordable luxury. Rating: 9 out of 10

25 October 2017

Petter Reinholdtsen: Locating IMDB IDs of movies in the Internet Archive using Wikidata

Recently, I needed to automatically check the copyright status of a set of The Internet Movie database (IMDB) entries, to figure out which one of the movies they refer to can be freely distributed on the Internet. This proved to be harder than it sounds. IMDB for sure list movies without any copyright protection, where the copyright protection has expired or where the movie is lisenced using a permissive license like one from Creative Commons. These are mixed with copyright protected movies, and there seem to be no way to separate these classes of movies using the information in IMDB. First I tried to look up entries manually in IMDB, Wikipedia and The Internet Archive, to get a feel how to do this. It is hard to know for sure using these sources, but it should be possible to be reasonable confident a movie is "out of copyright" with a few hours work per movie. As I needed to check almost 20,000 entries, this approach was not sustainable. I simply can not work around the clock for about 6 years to check this data set. I asked the people behind The Internet Archive if they could introduce a new metadata field in their metadata XML for IMDB ID, but was told that they leave it completely to the uploaders to update the metadata. Some of the metadata entries had IMDB links in the description, but I found no way to download all metadata files in bulk to locate those ones and put that approach aside. In the process I noticed several Wikipedia articles about movies had links to both IMDB and The Internet Archive, and it occured to me that I could use the Wikipedia RDF data set to locate entries with both, to at least get a lower bound on the number of movies on The Internet Archive with a IMDB ID. This is useful based on the assumption that movies distributed by The Internet Archive can be legally distributed on the Internet. With some help from the RDF community (thank you DanC), I was able to come up with this query to pass to the SPARQL interface on Wikidata:
SELECT ?work ?imdb ?ia ?when ?label
WHERE
 
  ?work wdt:P31/wdt:P279* wd:Q11424.
  ?work wdt:P345 ?imdb.
  ?work wdt:P724 ?ia.
  OPTIONAL  
        ?work wdt:P577 ?when.
        ?work rdfs:label ?label.
        FILTER(LANG(?label) = "en").
   
 
If I understand the query right, for every film entry anywhere in Wikpedia, it will return the IMDB ID and The Internet Archive ID, and when the movie was released and its English title, if either or both of the latter two are available. At the moment the result set contain 2338 entries. Of course, it depend on volunteers including both correct IMDB and The Internet Archive IDs in the wikipedia articles for the movie. It should be noted that the result will include duplicates if the movie have entries in several languages. There are some bogus entries, either because The Internet Archive ID contain a typo or because the movie is not available from The Internet Archive. I did not verify the IMDB IDs, as I am unsure how to do that automatically. I wrote a small python script to extract the data set from Wikidata and check if the XML metadata for the movie is available from The Internet Archive, and after around 1.5 hour it produced a list of 2097 free movies and their IMDB ID. In total, 171 entries in Wikidata lack the refered Internet Archive entry. I assume the 70 "disappearing" entries (ie 2338-2097-171) are duplicate entries. This is not too bad, given that The Internet Archive report to contain 5331 feature films at the moment, but it also mean more than 3000 movies are missing on Wikipedia or are missing the pair of references on Wikipedia. I was curious about the distribution by release year, and made a little graph to show how the amount of free movies is spread over the years: I expect the relative distribution of the remaining 3000 movies to be similar. If you want to help, and want to ensure Wikipedia can be used to cross reference The Internet Archive and The Internet Movie Database, please make sure entries like this are listed under the "External links" heading on the Wikipedia article for the movie:
*  Internet Archive film id=FightingLady 
*  IMDb title id=0036823 title=The Fighting Lady 
Please verify the links on the final page, to make sure you did not introduce a typo. Here is the complete list, if you want to correct the 171 identified Wikipedia entries with broken links to The Internet Archive: Q1140317, Q458656, Q458656, Q470560, Q743340, Q822580, Q480696, Q128761, Q1307059, Q1335091, Q1537166, Q1438334, Q1479751, Q1497200, Q1498122, Q865973, Q834269, Q841781, Q841781, Q1548193, Q499031, Q1564769, Q1585239, Q1585569, Q1624236, Q4796595, Q4853469, Q4873046, Q915016, Q4660396, Q4677708, Q4738449, Q4756096, Q4766785, Q880357, Q882066, Q882066, Q204191, Q204191, Q1194170, Q940014, Q946863, Q172837, Q573077, Q1219005, Q1219599, Q1643798, Q1656352, Q1659549, Q1660007, Q1698154, Q1737980, Q1877284, Q1199354, Q1199354, Q1199451, Q1211871, Q1212179, Q1238382, Q4906454, Q320219, Q1148649, Q645094, Q5050350, Q5166548, Q2677926, Q2698139, Q2707305, Q2740725, Q2024780, Q2117418, Q2138984, Q1127992, Q1058087, Q1070484, Q1080080, Q1090813, Q1251918, Q1254110, Q1257070, Q1257079, Q1197410, Q1198423, Q706951, Q723239, Q2079261, Q1171364, Q617858, Q5166611, Q5166611, Q324513, Q374172, Q7533269, Q970386, Q976849, Q7458614, Q5347416, Q5460005, Q5463392, Q3038555, Q5288458, Q2346516, Q5183645, Q5185497, Q5216127, Q5223127, Q5261159, Q1300759, Q5521241, Q7733434, Q7736264, Q7737032, Q7882671, Q7719427, Q7719444, Q7722575, Q2629763, Q2640346, Q2649671, Q7703851, Q7747041, Q6544949, Q6672759, Q2445896, Q12124891, Q3127044, Q2511262, Q2517672, Q2543165, Q426628, Q426628, Q12126890, Q13359969, Q13359969, Q2294295, Q2294295, Q2559509, Q2559912, Q7760469, Q6703974, Q4744, Q7766962, Q7768516, Q7769205, Q7769988, Q2946945, Q3212086, Q3212086, Q18218448, Q18218448, Q18218448, Q6909175, Q7405709, Q7416149, Q7239952, Q7317332, Q7783674, Q7783704, Q7857590, Q3372526, Q3372642, Q3372816, Q3372909, Q7959649, Q7977485, Q7992684, Q3817966, Q3821852, Q3420907, Q3429733, Q774474

24 October 2017

Iain R. Learmonth: Security by Obscurity

Today this blog post turned up on Hacker News, titled Obscurity is a Valid Security Layer . It makes some excellent points on the distinction between good and bad obscurity and it gives an example of good obscurity with SSH. From the post:
I configured my SSH daemon to listen on port 24 in addition to its regular port of 22 so I could see the difference in attempts to connect to each (the connections are usually password guessing attempts). My expected result is far fewer attempts to access SSH on port 24 than port 22, which I equate to less risk to my, or any, SSH daemon. I ran with this alternate port configuration for a single weekend, and received over eighteen thousand (18,000) connections to port 22, and five (5) to port 24.
Those of you that know me in the outside world will have probably heard me talk about how it s insane we have all these services running on the public Internet that don t need to be there, just waiting to be attacked. I have previously given a talk at TechMeetup Aberdeen where I talk about my use of Tor s Onion services to have services that only I should ever connect to be hidden from the general Internet. Onion services, especially the client authentication features, can also be useful for IoT dashboards and devices, allowing access from the Internet but via a secure and authenticated channel that is updated even when the IoT devices behind it have long been abandoned. If you re interested to learn more about Onion services, you could watch Roger Dingledine s talk from Def Con 25.

21 October 2017

Jaldhar Vyas: Sal Mubarak 2074

Wishing all Debian people a prosperous and auspicious Gujarati new year (V.S. 2074 called Saumya.) This year fireworks became legal for the first time in New Jersey. Not that it ever stopped us before but it is nice to see the government stop meddling for no reason. (Eff you, Indian Supreme Court.) Sparklers on Diwali. Although you can only see sparklers in the picture above, we got enough armament to make ISIS jealous. There were also lots of diabetes-inducing sweets and (inexpensive, practical) presents for young and old. That's what I call a proper Diwali and new year.

19 October 2017

Daniel Pocock: FOSDEM 2018 Real-Time Communications Call for Participation

FOSDEM is one of the world's premier meetings of free software developers, with over five thousand people attending each year. FOSDEM 2018 takes place 3-4 February 2018 in Brussels, Belgium. This email contains information about:
  • Real-Time communications dev-room and lounge,
  • speaking opportunities,
  • volunteering in the dev-room and lounge,
  • related events around FOSDEM, including the XMPP summit,
  • social events (the legendary FOSDEM Beer Night and Saturday night dinners provide endless networking opportunities),
  • the Planet aggregation sites for RTC blogs
Call for participation - Real Time Communications (RTC) The Real-Time dev-room and Real-Time lounge is about all things involving real-time communication, including: XMPP, SIP, WebRTC, telephony, mobile VoIP, codecs, peer-to-peer, privacy and encryption. The dev-room is a successor to the previous XMPP and telephony dev-rooms. We are looking for speakers for the dev-room and volunteers and participants for the tables in the Real-Time lounge. The dev-room is only on Sunday, 4 February 2018. The lounge will be present for both days. To discuss the dev-room and lounge, please join the FSFE-sponsored Free RTC mailing list. To be kept aware of major developments in Free RTC, without being on the discussion list, please join the Free-RTC Announce list. Speaking opportunities Note: if you used FOSDEM Pentabarf before, please use the same account/username Real-Time Communications dev-room: deadline 23:59 UTC on 30 November. Please use the Pentabarf system to submit a talk proposal for the dev-room. On the "General" tab, please look for the "Track" option and choose "Real Time Communications devroom". Link to talk submission. Other dev-rooms and lightning talks: some speakers may find their topic is in the scope of more than one dev-room. It is encouraged to apply to more than one dev-room and also consider proposing a lightning talk, but please be kind enough to tell us if you do this by filling out the notes in the form. You can find the full list of dev-rooms on this page and apply for a lightning talk at https://fosdem.org/submit Main track: the deadline for main track presentations is 23:59 UTC 3 November. Leading developers in the Real-Time Communications field are encouraged to consider submitting a presentation to the main track. First-time speaking? FOSDEM dev-rooms are a welcoming environment for people who have never given a talk before. Please feel free to contact the dev-room administrators personally if you would like to ask any questions about it. Submission guidelines The Pentabarf system will ask for many of the essential details. Please remember to re-use your account from previous years if you have one. In the "Submission notes", please tell us about:
  • the purpose of your talk
  • any other talk applications (dev-rooms, lightning talks, main track)
  • availability constraints and special needs
You can use HTML and links in your bio, abstract and description. If you maintain a blog, please consider providing us with the URL of a feed with posts tagged for your RTC-related work. We will be looking for relevance to the conference and dev-room themes, presentations aimed at developers of free and open source software about RTC-related topics. Please feel free to suggest a duration between 20 minutes and 55 minutes but note that the final decision on talk durations will be made by the dev-room administrators based on the received proposals. As the two previous dev-rooms have been combined into one, we may decide to give shorter slots than in previous years so that more speakers can participate. Please note FOSDEM aims to record and live-stream all talks. The CC-BY license is used. Volunteers needed To make the dev-room and lounge run successfully, we are looking for volunteers:
  • FOSDEM provides video recording equipment and live streaming, volunteers are needed to assist in this
  • organizing one or more restaurant bookings (dependending upon number of participants) for the evening of Saturday, 4 February
  • participation in the Real-Time lounge
  • helping attract sponsorship funds for the dev-room to pay for the Saturday night dinner and any other expenses
  • circulating this Call for Participation (text version) to other mailing lists
Related events - XMPP and RTC summits The XMPP Standards Foundation (XSF) has traditionally held a summit in the days before FOSDEM. There is discussion about a similar summit taking place on 2 February 2018. XMPP Summit web site - please join the mailing list for details. Social events and dinners The traditional FOSDEM beer night occurs on Friday, 2 February. On Saturday night, there are usually dinners associated with each of the dev-rooms. Most restaurants in Brussels are not so large so these dinners have space constraints and reservations are essential. Please subscribe to the Free-RTC mailing list for further details about the Saturday night dinner options and how you can register for a seat. Spread the word and discuss If you know of any mailing lists where this CfP would be relevant, please forward this email (text version). If this dev-room excites you, please blog or microblog about it, especially if you are submitting a talk. If you regularly blog about RTC topics, please send details about your blog to the planet site administrators:
Planet site Admin contact
All projects Free-RTC Planet (http://planet.freertc.org) contact planet@freertc.org
XMPP Planet Jabber (http://planet.jabber.org) contact ralphm@ik.nu
SIP Planet SIP (http://planet.sip5060.net) contact planet@sip5060.net
SIP (Espa ol) Planet SIP-es (http://planet.sip5060.net/es/) contact planet@sip5060.net
Please also link to the Planet sites from your own blog or web site as this helps everybody in the free real-time communications community. Contact For any private queries, contact us directly using the address fosdem-rtc-admin@freertc.org and for any other queries please ask on the Free-RTC mailing list. The dev-room administration team:

17 October 2017

Jonathan Dowland: Electric Dreams

No spoilers, for those who have yet to watch it... Channel 4 have been broadcasting a new 10-part series called Electric Dreams, based on some of the short fiction of Philip K Dick. The series was commissioned after Channel 4 lost Black Mirror to Netflix, perhaps to try and find something tonally similar. Electric Dreams is executive-produced by Brian Cranston, who also stars in one of the episodes yet to broadcast. I've read all of PKD's short fiction1 but it was a long time ago so I have mostly forgotten the stories upon which the series is based. I've quite enjoyed going back and re-reading them after watching the corresponding episodes to see what changes they've made. In some cases the changes are subtle or complementary, in other cases they've whittled the original story right out and installed a new one inside the shell. A companion compilation has been published with just the relevant short stories in it, and from what I've seen browsing it in a book shop it also contains short introductions which might be worth a read. Things started strong with The Hood Maker, which my wife also enjoyed, although she was disappointed to realise we wouldn't be revisiting those characters in the future. The world-building was strong enough that it seemed like a waste for a single episode. My favourite episode of those broadcast so far was The Commuter, starring Timothy Spall. The changes made were complementary and immensely expanded the emotional range of the story. In some ways, a key aspect of the original story was completely inverted, which I found quite funny: my original take on Dick's story was Dick implying a particular outcome was horrific, whereas it becomes desirable in the TV episode.
Episode 4, *Crazy Diamond* Episode 4, Crazy Diamond
One of the stories most hollowed-out was Sales Pitch which was the basis for Tony Grisoni s episode Crazy Diamond, starring Steve Buscemi and Sidse Babett Knudsen. Buscemi was good but Knudsen totally stole every frame she was in. Fans of the cancelled Channel 4 show Utopia should enjoy this one: both were directed by Marc Munden and the directing, photography and colour balance really recall it. The last episode broadcast was Real Life directed by Ronald D Moore of Battlestar Galactica reboot fame and starring Anna Paquin. Like Sales Pitch it bears very little resemblance to the original story. It played around with similar ideas explored in a lot of Sci-Fi movies and TV shows but left me a little flat; I didn't think it contributed much that I hadn't seen before. I was disappointed that there was a relatively conclusive ending. There was a subversive humour in the Dick short that was completely lost in the retelling. The world design seemed pretty generic. I'm looking forward to Autofac, which is one of the shorts I can remember particularly enjoying.

  1. as collected in the 5 volumes of The Collected Stories of Philip K Dick, although I don't doubt there are some stragglers that were missed out when that series was compiled.

Russ Allbery: Bundle haul

Confession time: I started making these posts (eons ago) because a close friend did as well, and I enjoyed reading them. But the main reason why I continue is because the primary way I have to keep track of the books I've bought and avoid duplicates is, well, grep on these posts. I should come up with a non-bullshit way of doing this, but time to do more elegant things is in short supply, and, well, it's my blog. So I'm boring all of you who read this in various places with my internal bookkeeping. I do try to at least add a bit of commentary. This one will be more tedious than most since it includes five separate Humble Bundles, which increases the volume a lot. (I just realized I'd forgotten to record those purchases from the past several months.) First, the individual books I bought directly: Ilona Andrews Sweep in Peace (sff)
Ilona Andrews One Fell Sweep (sff)
Steven Brust Vallista (sff)
Nicky Drayden The Prey of Gods (sff)
Meg Elison The Book of the Unnamed Midwife (sff)
Pat Green Night Moves (nonfiction)
Ann Leckie Provenance (sff)
Seanan McGuire Once Broken Faith (sff)
Seanan McGuire The Brightest Fell (sff)
K. Arsenault Rivera The Tiger's Daughter (sff)
Matthew Walker Why We Sleep (nonfiction)
Some new books by favorite authors, a few new releases I heard good things about, and two (Night Moves and Why We Sleep) from references in on-line articles that impressed me. The books from security bundles (this is mostly work reading, assuming I'll get to any of it), including a blockchain bundle: Wil Allsop Unauthorised Access (nonfiction)
Ross Anderson Security Engineering (nonfiction)
Chris Anley, et al. The Shellcoder's Handbook (nonfiction)
Conrad Barsky & Chris Wilmer Bitcoin for the Befuddled (nonfiction)
Imran Bashir Mastering Blockchain (nonfiction)
Richard Bejtlich The Practice of Network Security (nonfiction)
Kariappa Bheemaiah The Blockchain Alternative (nonfiction)
Violet Blue Smart Girl's Guide to Privacy (nonfiction)
Richard Caetano Learning Bitcoin (nonfiction)
Nick Cano Game Hacking (nonfiction)
Bruce Dang, et al. Practical Reverse Engineering (nonfiction)
Chris Dannen Introducing Ethereum and Solidity (nonfiction)
Daniel Drescher Blockchain Basics (nonfiction)
Chris Eagle The IDA Pro Book, 2nd Edition (nonfiction)
Nikolay Elenkov Android Security Internals (nonfiction)
Jon Erickson Hacking, 2nd Edition (nonfiction)
Pedro Franco Understanding Bitcoin (nonfiction)
Christopher Hadnagy Social Engineering (nonfiction)
Peter N.M. Hansteen The Book of PF (nonfiction)
Brian Kelly The Bitcoin Big Bang (nonfiction)
David Kennedy, et al. Metasploit (nonfiction)
Manul Laphroaig (ed.) PoC GTFO (nonfiction)
Michael Hale Ligh, et al. The Art of Memory Forensics (nonfiction)
Michael Hale Ligh, et al. Malware Analyst's Cookbook (nonfiction)
Michael W. Lucas Absolute OpenBSD, 2nd Edition (nonfiction)
Bruce Nikkel Practical Forensic Imaging (nonfiction)
Sean-Philip Oriyano CEHv9 (nonfiction)
Kevin D. Mitnick The Art of Deception (nonfiction)
Narayan Prusty Building Blockchain Projects (nonfiction)
Prypto Bitcoin for Dummies (nonfiction)
Chris Sanders Practical Packet Analysis, 3rd Edition (nonfiction)
Bruce Schneier Applied Cryptography (nonfiction)
Adam Shostack Threat Modeling (nonfiction)
Craig Smith The Car Hacker's Handbook (nonfiction)
Dafydd Stuttard & Marcus Pinto The Web Application Hacker's Handbook (nonfiction)
Albert Szmigielski Bitcoin Essentials (nonfiction)
David Thiel iOS Application Security (nonfiction)
Georgia Weidman Penetration Testing (nonfiction)
Finally, the two SF bundles: Buzz Aldrin & John Barnes Encounter with Tiber (sff)
Poul Anderson Orion Shall Rise (sff)
Greg Bear The Forge of God (sff)
Octavia E. Butler Dawn (sff)
William C. Dietz Steelheart (sff)
J.L. Doty A Choice of Treasons (sff)
Harlan Ellison The City on the Edge of Forever (sff)
Toh Enjoe Self-Reference ENGINE (sff)
David Feintuch Midshipman's Hope (sff)
Alan Dean Foster Icerigger (sff)
Alan Dean Foster Mission to Moulokin (sff)
Alan Dean Foster The Deluge Drivers (sff)
Taiyo Fujii Orbital Cloud (sff)
Hideo Furukawa Belka, Why Don't You Bark? (sff)
Haikasoru (ed.) Saiensu Fikushon 2016 (sff anthology)
Joe Haldeman All My Sins Remembered (sff)
Jyouji Hayashi The Ouroboros Wave (sff)
Sergei Lukyanenko The Genome (sff)
Chohei Kambayashi Good Luck, Yukikaze (sff)
Chohei Kambayashi Yukikaze (sff)
Sakyo Komatsu Virus (sff)
Miyuki Miyabe The Book of Heroes (sff)
Kazuki Sakuraba Red Girls (sff)
Robert Silverberg Across a Billion Years (sff)
Allen Steele Orbital Decay (sff)
Bruce Sterling Schismatrix Plus (sff)
Michael Swanwick Vacuum Flowers (sff)
Yoshiki Tanaka Legend of the Galactic Heroes, Volume 1: Dawn (sff)
Yoshiki Tanaka Legend of the Galactic Heroes, Volume 2: Ambition (sff)
Yoshiki Tanaka Legend of the Galactic Heroes, Volume 3: Endurance (sff)
Tow Ubukata Mardock Scramble (sff)
Sayuri Ueda The Cage of Zeus (sff)
Sean Williams & Shane Dix Echoes of Earth (sff)
Hiroshi Yamamoto MM9 (sff)
Timothy Zahn Blackcollar (sff)
Phew. Okay, all caught up, and hopefully won't have to dump something like this again in the near future. Also, more books than I have any actual time to read, but what else is new.

15 October 2017

Norbert Preining: TeX Live Manager: JSON output

With the development of TLCockpit continuing, I found the need for and easy exchange format between the TeX Live Manager tlmgr and frontend programs like TLCockpit. Thus, I have implemented JSON output for the tlmgr info command. While the format is not 100% stable I might change some thing I consider it pretty settled. The output of tlmgr info --data json is a JSON array with JSON objects for each package requested (default is to list all).
[ TLPackageObj, TLPackageObj, ... ]
The structure of the JSON object TLPackageObj reflects the internal Perl hash. Guaranteed to be present keys are name (String) and avilable (Boolean). In case the package is available, there are the following further keys sorted by their type: A rather long example showing the output for the package latex, formatted with json_pp and having the list of files and the long description shortened:
[
    
      "installed" : true,
      "doccontainerchecksum" : "5bdfea6b85c431a0af2abc8f8df160b297ad73f6a324ca88df990f01f24611c9ae80d2f6d12c7b3767308fbe3de3fca3d11664b923ea4080fb13fd056a1d0c3d",
      "docfiles" : [
         "texmf-dist/doc/latex/base/README.txt",
         ....
         "texmf-dist/doc/latex/base/webcomp.pdf"
      ],
      "containersize" : 163892,
      "depends" : [
         "luatex",
         "pdftex",
         "latexconfig",
         "latex-fonts"
      ],
      "runsize" : 414,
      "relocated" : false,
      "doccontainersize" : 12812184,
      "srcsize" : 752,
      "revision" : 43813,
      "srcfiles" : [
         "texmf-dist/source/latex/base/alltt.dtx",
         ....
         "texmf-dist/source/latex/base/utf8ienc.dtx"
      ],
      "category" : "Package",
      "cataloguedata" :  
         "version" : "2017/01/01 PL1",
         "topics" : "format",
         "license" : "lppl1.3",
         "date" : "2017-01-25 23:33:57 +0100"
       ,
      "srccontainerchecksum" : "1d145b567cf48d6ee71582a1f329fe5cf002d6259269a71d2e4a69e6e6bd65abeb92461d31d7137f3803503534282bc0c5546e5d2d1aa2604e896e607c53b041",
      "postactions" : [],
      "binsize" :  ,
      "longdesc" : "LaTeX is a widely-used macro package for TeX, [...]",
      "srccontainersize" : 516036,
      "containerchecksum" : "af0ac85f89b7620eb7699c8bca6348f8913352c473af1056b7a90f28567d3f3e21d60be1f44e056107766b1dce8d87d367e7f8a82f777d565a2d4597feb24558",
      "executes" : [],
      "binfiles" :  ,
      "name" : "latex",
      "catalogue" : null,
      "docsize" : 3799,
      "available" : true,
      "runfiles" : [
         "texmf-dist/makeindex/latex/gglo.ist",
         ...
         "texmf-dist/tex/latex/base/x2enc.dfu"
      ],
      "shortdesc" : "A TeX macro package that defines LaTeX"
    
]
What is currently not available via tlmgr info and thus also not via the JSON output is access to virtual TeX Live databases with several member databases (multiple repositories). I am thinking about how to incorporate this information. These changes are currently available in the tlcritical repository, but will enter proper TeX Live repositories soon. Using this JSON output I will rewrite the current TLCockpit tlmgr interface to display more complete information.

14 October 2017

Norbert Preining: ScalaFX: ListView with CellFactory

I had a bit hard time to get ScalaFX to display a list of items in a scrollable space, and each item can be clicked. I use this in TLCockpit to display the list of documentation files in a TeX Live package, and open it directly from the application. Unfortunately there is not a huge amount of examples using ScalaFX out there in the web, so it took me a bit. My first try was using a VBox with various Labels in there, but this is not scrollable. In other areas I have used TreeTableView, so in this case using ListView should be fine. What I finally came up is the following code:
import scalafx.application.JFXApp
import scalafx.application.JFXApp.PrimaryStage
import scalafx.collections.ObservableBuffer
import scalafx.geometry.Orientation
import scalafx.scene.control. ListCell, ListView 
import scalafx.scene.input.MouseEvent
import scalafx.scene. Cursor, Scene 
import scalafx.scene.paint.Color
import scalafx.Includes._
object ApplicationMain extends JFXApp  
  val SomeStrings: Seq[String] = Seq("Hello", "World", "Enjoy")
  stage = new PrimaryStage  
    title = "ListViewExample"
    scene = new Scene  
      root =  
        new ListView[String]  
          orientation = Orientation.Vertical
          cellFactory =  
            p =>  
              val cell = new ListCell[String]
              cell.textFill = Color.Blue
              cell.cursor = Cursor.Hand
              cell.item.onChange   (_, _, str) => cell.text = str  
              cell.onMouseClicked =   me: MouseEvent => println("Do something with " + cell.text.value)  
              cell
             
           
          items = ObservableBuffer(SomeStrings)
         
       
     
   
 
Some comments to the code, at least as far I understand it: Once managed, it doesn t look so complicated, but took me some time.

13 October 2017

Shirish Agarwal: I need to speak up now X Economics

Dear all, This would be a longish blog post (as most of mine are) compiled over days but as there is so short a time and so much to share. I had previously thought to share beautiful photographs of Ganesh mandals taking out the procession at time of immersion of the idol or the last day of Durga Puja recent events around do not make my mood to share photos at this point in time. I may share some of them in a future blog post or two . Before going further, I would like to offer my sympathies and condolences to people hurt and dislocated in Hurricane Irma , the 2017 Central Mexico Earthquake and lastly the most recent Las Vegas shooting as well as Hurricane Maria in Puerto Rico . I am somewhat nonplussed as to why Americans always want to name, especially hurricanes which destroy people s lives and livelihood built over generations and why most of the hurricanes are named after women. A look at weather.com site unveiled the answer to the mystery. Ironically (or not) I saw some of the best science coverage about Earthquakes or anything scientific reporting and analysis after a long time in mainstream newspapers in India. On another note, I don t understand or even expect to understand why the gunman did what he did 2 days back. Country music AFAIK is one of the most chilled-out kind of music, in some ways very similar to classical Indian singing although they are worlds apart in style of singing, renditions, artists, the way they emote etc. I seriously wish that the gunman had not been shot but caught and reasons were sought about what he did, he did. While this is certainly armchair thinking as was not at the scene of crime, but if a Mumbai Police constable could do it around a decade ago armed only with a lathi could do it, why couldn t the American cops who probably are trained in innumerable ways to subdue people without killing them, did. While investigations are on, I suspect if he were caught just like Ajmal Kasab was caught then lot of revelations might have come up. From what is known, the gentleman was upwardly mobile i.e. he was white, rich and apparently had no reason to have beef with anybody especially a crowd swaying to some nice music, all of which makes absolutely no sense. Indian Economy Slowdown Anyways, back to one of the main reasons of writing this blog post. Few days back, an ex-finance Minister of India Yashwant Sinha wrote what was felt by probably millions of Indians, an Indian Express article called I need to speak up now While there have been many, many arguments made since then by various people. A simple search of I need to speak up would lead to lead to many a result besides the one I have shared above. The only exception I have with the article is the line Forty leading companies of the country are already facing bankruptcy proceedings. Many more are likely to follow suit. I would not bore you but you ask any entrepreneur trying to set up shop in India i.e. ones who actually go through the processes of getting all the licenses for setting up even a small businesses as to the numerous hurdles they have to overcome and laid-back corrupt bureaucracy which they have to overcome. I could have interviewed some of my friends who had the conviction and the courage to set up shop and spent more than half a decade getting all the necessary licenses and approval to set up but it probably would be too specific for one industry or the other and would lead to the same result. Co-incidentally, a new restaurant, leaf opened in my vicinity few weeks before. From the looks it looked like a high-brow, high-priced restaurant hence like many others I did not venture in. After a few days, they introduced south-Indian delicacies like Masala Dosa, Uttapam at prices similar to other restaurants around. So I ventured in and bought some south Indian food to consume between mum and me. Few days later, I became friends with the owner/franchisee and I suggested (in a friendly tone) that why he doesn t make it like a CCD play where many people including yours truly use the service to share, strategize and meet with clients. The CCD joints usually serve coffee and snacks (which are over-priced but still run out pretty fast) but people come as they have chilled-out atmosphere and Wi-Fi access which people need for their smartphones, although the Wi-Fi part may soon become redundant With Reliance Jio making a big play. I also shared why he doesn t add more variety and time (the south Indian items are time-limited) as I see/saw many empty chairs there. Anyways, the shop-owner/franchisee shared his gross costs including salary, stocking, electricity, rent and it doesn t pan out to be serving Rs.80/- dish (roughly a 1US dollar and 25 cents) then serving INR Rs. 400/- a dish (around 6 $USD). One round of INR 400/- + dishes make his costs for the day, around 12 tables were there. It s when they have two full rounds of dishes costing INR 400/- or more that he actually has profits and he is predicting loss for at least 6 months to a year before he makes a rebound. He needs steady customers rather than just walk-ins that will make his business work/click. Currently his family is bearing the costs. He didn t mention the taxes although I know apart from GST there are still some local body taxes that they will have to pay and comply with. There are a multitude of problems for shutting a shop legally as well as they have to again renavigate the bureaucracy for the same. I have seen more than a few retailers downing their shutters for 6-8 months and then either sell it to new management, let go of the lease or simply sell the property to a competitor. The Insolvency and Bankruptcy Code is probably the first proper exit policy for large companies. So the 40 odd companies that Mr. Sinha were talking about were probably sick for a long time. In India, there is also an additional shame of being a failed entrepreneur unlike in the west where Entrepreneurs start on their next venture. As seen from Retailing In India only 3.3% of the population or at the most 4% of the population is directly or indirectly linked with the retail trade. Most of the economy still derives its wealth from the agrarian sector which is still reeling under the pressure from demonetization which happened last year. Al jazeera surprisingly portrayed a truer picture of the effects demonetization had on common citizen than many Indian newspapers did at the time. Because of the South African Debconf, I had to resort to debit cards and hence was able to escape standing in long lines in which many an old and women perished. It is only yesterday that the Government has acknowledged which many prominent Indians have been saying for months now, that we are in a slowdown . Be aware of the terms being used for effect by the Prime Minister. There are two articles which outlines the troubles India is in atm. The only bright spot has been e-commerce which so far has eluded GST although the Govt. has claimed regulations to put it in check. Indian Education System Interestingly, Ravish Kumar has started a series on NDTV where he is showcasing how Indian education sector, especially public colleges have been left to teachers on contract basis, see the first four episodes on NDTV channel starting with the first one I have shared as a hyperlink. I apologize as the series is in Hindi as the channel is meant for Indians and is mostly limited to Northern areas of the Country (mostly) although he has been honest that it is because they lack resources to tackle the amount of information flowing to them. Ravish started the series with sharing information about the U.S. where the things are similar with some teachers needing to sleep in cars because of high-cost of living to some needing to turn to sex-work . I was shocked when I read the guardian article, that is no way to treat our teachers.I went on to read How the American University was Killed following the breadcrumbs along the way. Reading that it seems Indians have been following the American system playbook from the 1980 s itself. The article talks about HMO as well and that seems to have followed here as well with my own experience of hospital fees and drugs which I had to entail a few weeks/month ago. Few years ago, when me and some of my friends had the teaching bug and we started teaching in a nearby municipal school, couple of teachers had shared that they were doing 2-3 jobs to make ends meet. I don t know about others in my group, at least I was cynical because I thought all the teachers were permanent and they make good money only to realize now that the person was probably speaking the truth. When you have to do three jobs to make ends meet from where do you bring the passion to teach young people and that too outside the syllabus ? Also, with this new knowledge in hindsight, I take back all my comments I made last year and the year before for the pathetic education being put up by the State. With teachers being paid pathetically/underpaid and almost 60% teachers being ad-hoc/adjunct teachers they have to find ways to have some sense of security. Most teachers are bachelors as they are poor and cannot offer any security (either male or female) and for women, after marriage it actually makes no sense for them to continue in this profession. I salute all the professors who are ad-hoc in nature and probably will never get a permanent position in their life. I think in some way, thanx to him, that the government has chosen to give 7th pay commisson salary to teachers. While the numbers may appear be large, there are a lot of questions as to how many people will actually get paid. There needs to be lot of vacancies which need to be filled quickly but don t see any solution in the next 2-3 years as well. The Government has taken a position to use/re-hire retired teachers rather than have new young teachers as an unwritten policy. In this Digital India context how are retired teachers supposed to understand and then pass on digital concepts is beyond me when at few teacher trainings I have seen they lack even the most basic knowledge that I learnt at least a decade or two ago, the difference is that vast. I just don t know what to say to that. My own experience with my own mother who had pretty good education in her time and probably would have made a fine business-woman if she knew that she will have a child that she would have to raise by herself alone (along with maternal grand-parents) is testimonial to the fact how hard it is for older people to grasp technology and here I m talking just using the interface as a consumer rather than a producer or someone in-between who has the idea of how companies and governments profit from whatever data is shared one way or the other. After watching the series/episodes and discussing the issue with my mother it was revealed that both her and my late maternal grandfather were on casual/ad-hoc basis till 20-25 years in their service in the defense sector. If Ravish were to do a series on the defense sector he probably would find the same thing there. To add to that, the defense sector is a vital component to a country s security. If 60% of the defense staff in all defense establishments have temporary staff how do you ensure the loyalty of the people working therein. That brings to my mind Ignorance is bliss . Software development and deployment There is another worry that all are skirting around, the present dispensation/government s mantra is minimum government-maximum governance with digital technologies having all solutions which is leading to massive unemployment. Also from most of the stories/incidents I read in the newspapers, mainstream media and elsewhere it seems most software deployments done in India are done without having any system of internal checks and balances. There is no lintian for software to be implemented. Contracts seem to be given to big companies and there is no mention of what prerequisites or conditions were laid down by the Government for software development and deployment and if any checks were done to ensure that the software being developed was in according to government specifications or not. Ideally this should all be in public domain so that questions can be asked and responsibility fixed if things go haywire, as currently they do not. Software issues As my health been not that great, I have been taking a bit more time and depth while filing bugs. #877638 is a good example. I suspect though that part of the problem might be that mate has moved to gtk3 while guake still has gtk-2 bindings. I also reported the issue upstream both in mate-panel as well as guake . I haven t received any response from either or/and upstreams . I also have been fiddling around with gdb to better understand the tool so I can exploit/use this tool in a better way. There are some commands within the gdb interface which seem to be interesting and hopefully I ll try how the commands perform over days, weeks to a month. I hope we see more action on the mate-panel/guake bug as well as move of guake to gtk+3 but that what seemingly seemed like wait for eternity seems to have done by somebody in last couple of days. As shared in the ticket there are lots of things still to do but it seems the heavy lifting has been done but seems merging will be tricky as two developers have been trying to update to gtk+3 although aichingm seems to have a leg up with his 3! branch. Another interesting thing I saw is the below picture. Firefox is out of date on wordpress.com The firefox version I was using to test the site/wordpress-wp-admin was Mozilla Firefox 52.4.0 which AFAIK is a pretty recentish one and people using Debian stretch would probably be using the same version (firefox stable/LTS) rather than the more recent versions. I went to the link it linked to and it gave no indication as to why it thought my browser is out-of-date and what functionality was/is missing. I have found that wordpress support has declined quite a bit and people don t seem to use the forums as much as they used to before. I also filed a few bugs for qalculate. #877716 where a supposedly transitional package removes the actual application, #877717 as the software has moved its repo. to github.com as well as tickets and other things in process and lastly #877733. I had been searching for a calculator which can do currency calculations on the fly (say for e.g. doing personal budgeting for Taiwan debconf) without needing to manually enter the conversion rates and losing something in the middle. While the current version has support for some limited currencies, the new versions promise more as other people probably have more diverse needs for currency conversions (people who do long or short on oil, stocks overseas is just one example, I am sure there are many others) than simplistic mine.
Filed under: Miscellenous Tagged: #American Education System, #bug-filing, #Climate change, #Dignity, #e-commerce, #gtk+3, #gtk2, #Indian Economy 'Slowdown', #Indian Education System, #Insolvency and Bankruptcy Code, #Las Vegas shooting, #Modern Retail in India, #planet-debian, #qalculate, Ad-hoc and Adjunct Professors, wordpress.com

12 October 2017

Joachim Breitner: Isabelle functions: Always total, sometimes undefined

Often, when I mention how things work in the interactive theorem prover [Isabelle/HOL] (in the following just Isabelle 1) to people with a strong background in functional programming (whether that means Haskell or Coq or something else), I cause confusion, especially around the issue of what is a function, are function total and what is the business with undefined. In this blog post, I want to explain some these issues, aimed at functional programmers or type theoreticians. Note that this is not meant to be a tutorial; I will not explain how to do these things, and will focus on what they mean.

HOL is a logic of total functions If I have a Isabelle function f :: a b between two types a and b (the function arrow in Isabelle is , not ), then by definition of what it means to be a function in HOL whenever I have a value x :: a, then the expression f x (i.e. f applied to x) is a value of type b. Therefore, and without exception, every Isabelle function is total. In particular, it cannot be that f x does not exist for some x :: a. This is a first difference from Haskell, which does have partial functions like
spin :: Maybe Integer -> Bool
spin (Just n) = spin (Just (n+1))
Here, neither the expression spin Nothing nor the expression spin (Just 42) produce a value of type Bool: The former raises an exception ( incomplete pattern match ), the latter does not terminate. Confusingly, though, both expressions have type Bool. Because every function is total, this confusion cannot arise in Isabelle: If an expression e has type t, then it is a value of type t. This trait is shared with other total systems, including Coq. Did you notice the emphasis I put on the word is here, and how I deliberately did not write evaluates to or returns ? This is because of another big source for confusion:

Isabelle functions do not compute We (i.e., functional programmers) stole the word function from mathematics and repurposed it2. But the word function , in the context of Isabelle, refers to the mathematical concept of a function, and it helps to keep that in mind. What is the difference?
  • A function a b in functional programming is an algorithm that, given a value of type a, calculates (returns, evaluates to) a value of type b.
  • A function a b in math (or Isabelle) associates with each value of type a a value of type b.
For example, the following is a perfectly valid function definition in math (and HOL), but could not be a function in the programming sense:
definition foo :: "(nat   real)   real" where
  "foo seq = (if convergent seq then lim seq else 0)"
This assigns a real number to every sequence, but it does not compute it in any useful sense. From this it follows that

Isabelle functions are specified, not defined Consider this function definition:
fun plus :: "nat   nat   nat"  where
   "plus 0       m = m"
   "plus (Suc n) m = Suc (plus n m)"
To a functional programmer, this reads
plus is a function that analyses its first argument. If that is 0, then it returns the second argument. Otherwise, it calls itself with the predecessor of the first argument and increases the result by one.
which is clearly a description of a computation. But to Isabelle, the above reads
plus is a binary function on natural numbers, and it satisfies the following two equations:
And in fact, it is not so much Isabelle that reads it this way, but rather the fun command, which is external to the Isabelle logic. The fun command analyses the given equations, constructs a non-recursive definition of plus under the hood, passes that to Isabelle and then proves that the given equations hold for plus. One interesting consequence of this is that different specifications can lead to the same functions. In fact, if we would define plus' by recursing on the second argument, we d obtain the the same function (i.e. plus = plus' is a theorem, and there would be no way of telling the two apart).

Termination is a property of specifications, not functions Because a function does not evaluate, it does not make sense to ask if it terminates. The question of termination arises before the function is defined: The fun command can only construct plus in a way that the equations hold if it passes a termination check very much like Fixpoint in Coq. But while the termination check of Fixpoint in Coq is a deep part of the basic logic, in Isabelle it is simply something that this particular command requires for its internal machinery to go through. At no point does a termination proof of the function exist as a theorem inside the logic. And other commands may have other means of defining a function that do not even require such a termination argument! For example, a function specification that is tail-recursive can be turned in to a function, even without a termination proof: The following definition describes a higher-order function that iterates its first argument f on the second argument x until it finds a fixpoint. It is completely polymorphic (the single quote in 'a indicates that this is a type variable):
partial_function (tailrec)
  fixpoint :: "('a   'a)   'a   'a"
where
  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
We can work with this definition just fine. For example, if we instantiate f with ( x. x-1), we can prove that it will always return 0:
lemma "fixpoint (  n . n - 1) (n::nat) = 0"
  by (induction n) (auto simp add: fixpoint.simps)
Similarly, if we have a function that works within the option monad (i.e. Maybe in Haskell), its specification can always be turned into a function without an explicit termination proof here one that calculates the Collatz sequence:
partial_function (option) collatz :: "nat   nat list option"
 where "collatz n =
        (if n = 1 then Some [n]
         else if even n
           then do   ns <- collatz (n div 2);    Some (n # ns)  
           else do   ns <- collatz (3 * n + 1);  Some (n # ns) )"
Note that lists in Isabelle are finite (like in Coq, unlike in Haskell), so this function returns a list only if the collatz sequence eventually reaches 1. I expect these definitions to make a Coq user very uneasy. How can fixpoint be a total function? What is fixpoint ( n. n+1)? What if we run collatz n for a n where the Collatz sequence does not reach 1?3 We will come back to that question after a little detour

HOL is a logic of non-empty types Another big difference between Isabelle and Coq is that in Isabelle, every type is inhabited. Just like the totality of functions, this is a very fundamental fact about what HOL defines to be a type. Isabelle gets away with that design because in Isabelle, we do not use types for propositions (like we do in Coq), so we do not need empty types to denote false propositions. This design has an important consequence: It allows the existence of a polymorphic expression that inhabits any type, namely
undefined :: 'a
The naming of this term alone has caused a great deal of confusion for Isabelle beginners, or in communication with users of different systems, so I implore you to not read too much into the name. In fact, you will have a better time if you think of it as arbitrary or, even better, unknown. Since undefined can be instantiated at any type, we can instantiate it for example at bool, and we can observe an important fact: undefined is not an extra value besides the usual ones . It is simply some value of that type, which is demonstrated in the following lemma:
lemma "undefined = True   undefined = False" by auto
In fact, if the type has only one value (such as the unit type), then we know the value of undefined for sure:
lemma "undefined = ()" by auto
It is very handy to be able to produce an expression of any type, as we will see as follows

Partial functions are just underspecified functions For example, it allows us to translate incomplete function specifications. Consider this definition, Isabelle s equivalent of Haskell s partial fromJust function:
fun fromSome :: "'a option   'a" where
  "fromSome (Some x) = x"
This definition is accepted by fun (albeit with a warning), and the generated function fromSome behaves exactly as specified: when applied to Some x, it is x. The term fromSome None is also a value of type 'a, we just do not know which one it is, as the specification does not address that. So fromSome None behaves just like undefined above, i.e. we can prove
lemma "fromSome None = False   fromSome None = True" by auto
Here is a small exercise for you: Can you come up with an explanation for the following lemma:
fun constOrId :: "bool   bool" where
  "constOrId True = True"
lemma "constOrId = ( _.True)   constOrId = ( x. x)"
  by (metis (full_types) constOrId.simps)
Overall, this behavior makes sense if we remember that function definitions in Isabelle are not really definitions, but rather specifications. And a partial function definition is simply a underspecification. The resulting function is simply any function hat fulfills the specification, and the two lemmas above underline that observation.

Nonterminating functions are also just underspecified Let us return to the puzzle posed by fixpoint above. Clearly, the function seen as a functional program is not total: When passed the argument ( n. n + 1) or ( b. b) it will loop forever trying to find a fixed point. But Isabelle functions are not functional programs, and the definitions are just specifications. What does the specification say about the case when f has no fixed-point? It states that the equation fixpoint f x = fixpoint f (f x) holds. And this equation has a solution, for example fixpoint f _ = undefined. Or more concretely: The specification of the fixpoint function states that fixpoint ( b. b) True = fixpoint ( b. b) False has to hold, but it does not specify which particular value (True or False) it should denote any is fine.

Not all function specifications are ok At this point you might wonder: Can I just specify any equations for a function f and get a function out of that? But rest assured: That is not the case. For example, no Isabelle command allows you define a function bogus :: () nat with the equation bogus () = Suc (bogus ()), because this equation does not have a solution. We can actually prove that such a function cannot exist:
lemma no_bogus: "  bogus. bogus () = Suc (bogus ())" by simp
(Of course, not_bogus () = not_bogus () is just fine )

You cannot reason about partiality in Isabelle We have seen that there are many ways to define functions that one might consider partial . Given a function, can we prove that it is not partial in that sense? Unfortunately, but unavoidably, no: Since undefined is not a separate, recognizable value, but rather simply an unknown one, there is no way of stating that A function result is not specified . Here is an example that demonstrates this: Two partial functions (one with not all cases specified, the other one with a self-referential specification) are indistinguishable from the total variant:
fun partial1 :: "bool   unit" where
  "partial1 True = ()"
partial_function (tailrec) partial2 :: "bool   unit" where
  "partial2 b = partial2 b"
fun total :: "bool   unit" where
  "total True = ()"
  "total False = ()"
lemma "partial1 = total   partial2 = total" by auto
If you really do want to reason about partiality of functional programs in Isabelle, you should consider implementing them not as plain HOL functions, but rather use HOLCF, where you can give equational specifications of functional programs and obtain continuous functions between domains. In that setting, () and partial2 = total. We have done that to verify some of HLint s equations.

You can still compute with Isabelle functions I hope by this point, I have not scared away anyone who wants to use Isabelle for functional programming, and in fact, you can use it for that. If the equations that you pass to fun are a reasonable definition for a function (in the programming sense), then these equations, used as rewriting rules, will allow you to compute that function quite like you would in Coq or Haskell. Moreover, Isabelle supports code extraction: You can take the equations of your Isabelle functions and have them expored into Ocaml, Haskell, Scala or Standard ML. See Concon for a conference management system with confidentially verified in Isabelle. While these usually are the equations you defined the function with, they don't have to: You can declare other proved equations to be used for code extraction, e.g. to refine your elegant definitions to performant ones. Like with code extraction from Coq to, say, Haskell, the adequacy of the translations rests on a moral reasoning foundation. Unlike extraction from Coq, where you have an (unformalized) guarantee that the resulting Haskell code is terminating, you do not get that guarantee from Isabelle. Conversely, this allows you do reason about and extract non-terminating programs, like fixpoint, which is not possible in Coq. There is currently ongoing work about verified code generation, where the code equations are reflected into a deep embedding of HOL in Isabelle that would allow explicit termination proofs.

Conclusion We have seen how in Isabelle, every function is total. Function declarations have equations, but these do not define the function in an computational sense, but rather specify them. Because in HOL, there are no empty types, many specifications that appear partial (incomplete patterns, non-terminating recursion) have solutions in the space of total functions. Partiality in the specification is no longer visible in the final product.

PS: Axiom undefined in Coq This section is speculative, and an invitation for discussion. Coq already distinguishes between types used in programs (Set) and types used in proofs Prop. Could Coq ensure that every t : Set is non-empty? I imagine this would require additional checks in the Inductive command, similar to the checks that the Isabelle command datatype has to perform4, and it would disallow Empty_set. If so, then it would be sound to add the following axiom
Axiom undefined : forall (a : Set), a.
wouldn't it? This axiom does not have any computational meaning, but that seems to be ok for optional Coq axioms, like classical reasoning or function extensionality. With this in place, how much of what I describe above about function definitions in Isabelle could now be done soundly in Coq. Certainly pattern matches would not have to be complete and could sport an implicit case _ undefined. Would it help with non-obviously terminating functions? Would it allow a Coq command Tailrecursive that accepts any tailrecursive function without a termination check?

  1. Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.
  2. Isabelle is a metalogical framework, and other logics, e.g. Isabelle/ZF, behave differently. For the purpose of this blog post, I always mean Isabelle/HOL.
  3. Let me know if you find such an n. Besides n = 0.
  4. Like fun, the constructions by datatype are not part of the logic, but create a type definition from more primitive notions that is isomorphic to the specified data type.

08 October 2017

Daniel Pocock: A step change in managing your calendar, without social media

Have you been to an event recently involving free software or a related topic? How did you find it? Are you organizing an event and don't want to fall into the trap of using Facebook or Meetup or other services that compete for a share of your community's attention? Are you keen to find events in foreign destinations related to your interest areas to coincide with other travel intentions? Have you been concerned when your GSoC or Outreachy interns lost a week of their project going through the bureaucracy to get a visa for your community's event? Would you like to make it easier for them to find the best events in the countries that welcome and respect visitors? In many recent discussions about free software activism, people have struggled to break out of the illusion that social media is the way to cultivate new contacts. Wouldn't it be great to make more meaningful contacts by attending more a more diverse range of events rather than losing time on social media? Making it happen There are already a number of tools (for example, Drupal plugins and Wordpress plugins) for promoting your events on the web and in iCalendar format. There are also a number of sites like Agenda du Libre and GriCal who aggregate events from multiple communities where people can browse them. How can we take these concepts further and make a convenient, compelling and global solution? Can we harvest event data from a wide range of sources and compile it into a large database using something like PostgreSQL or a NoSQL solution or even a distributed solution like OpenDHT? Can we use big data techniques to mine these datasources and help match people to events without compromising on privacy? Why not build an automated iCalendar "to-do" list of deadlines for events you want to be reminded about, so you never miss the deadlines for travel sponsorship or submitting a talk proposal? I've started documenting an architecture for this on the Debian wiki and proposed it as an Outreachy project. It will also be offered as part of GSoC in 2018. Ways to get involved If you would like to help this project, please consider introducing yourself on the debian-outreach mailing list and helping to mentor or refer interns for the project. You can also help contribute ideas for the specification through the mailing list or wiki. Mini DebConf Prishtina 2017 This weekend I've been at the MiniDebConf in Prishtina, Kosovo. It has been hosted by the amazing Prishtina hackerspace community. Watch out for future events in Prishtina, the pizzas are huge, but that didn't stop them disappearing before we finished the photos:

01 October 2017

Paul Wise: FLOSS Activities September 2017

Changes

Issues

Review

Administration
  • icns: merged patches
  • Debian: help guest user with access, investigate/escalate broken network, restart broken stunnels, investigate static.d.o storage, investigate weird RAID mails, ask hoster to investigate power issue,
  • Debian mentors: lintian/security updates & reboot
  • Debian wiki: merged & deployed patch, redirect DDTSS translator, redirect user support requests, whitelist email addresses, update email for accounts with bouncing email,
  • Debian derivatives census: merged/deployed patches
  • Debian PTS: debugged cron mails, deployed changes, reran scripts, fixed configuration file
  • Openmoko: debug reboot issue, debug load issues

Communication

Sponsors The samba bug was sponsored by my employer. All other work was done on a volunteer basis.

Next.