24 Apr 2018

feedPlanet Debian

Carl Chenet: Use Nginx Unit 1.0 with your Django project on Debian Stretch

Nginx Unit 1.0 was released 2018, April the 12th. It is a new application server written by the Nginx team.

Some features are really interesting, such as:

I was setting up a new Django project at this time and it was a great opportunity to start using Unit. It has some unexpected pitfalls to install and configure.

1. Installing Nginx Unit for Django

Installing Unit is quite straightforward. I use a Debian Stretch. If you have another system, have a look at the official documentation.

If you install Unit on a dedicated server using a grsecurity kernel, it won't work. Using the kernel of your GNU/Linux distributions solves this issue.

First we need to get the key of the remote Debian Nginx repository:

# wget -q -O - https://nginx.org/keys/nginx_signing.key | apt-key add

Next, create the /etc/apt/sources.list.d/unit.list file with the following lines:

deb https://packages.nginx.org/unit/debian/ stretch unit
deb-src https://packages.nginx.org/unit/debian/ stretch unit

Now update your list of repositories, install Nginx Unit and the module for Python 3:

# apt-get update
# apt install unit unit-python3.5

Now activate the Systemd unit service (yep, confusing, poor name choice IMO) and start Nginx Unit :

# systemctl enable unit
# systemctl start unit
# systemctl status unit
 ● unit.service - NGINX Unit
 Loaded: loaded (/lib/systemd/system/unit.service; enabled; vendor preset: enabled)
 Active: active (running) since Sat 2018-04-21 16:51:31 CEST; 18h ago

2. Configure Nginx Unit

In order to configure Unit, you need to write a JSON file and post it to the Unit sock file on your server.

Here is my JSON configuration:

{
 "listeners": {
   "127.0.0.1:8300": {
   "application": "myapp"
   }
 },

"applications": {
  "myapp": {
    "type": "python",
    "processes": 5,
    "module": "myapp.wsgi",
    "user": "myapp",
    "group": "myapp",
    "path": "/home/myapp/prod/myapp"
    }
   }
 }

Ok, here is a pitfall. You need to understand that Unit will use the path parameter as your application root, then try to load the wsgi.py from the module parameter. So here it means that my wsgi.py is located in /home/myapp/prod/myapp/myapp/wsgi.py

Now we're ready to inject our Unit configuration with curl:

# curl -X PUT -d @myapp.unit.json --unix-socket /var/run/control.unit.sock http://localhost/
{
 "success": "Reconfiguration done."
}

Great, now we need our good ol' Nginx web server as a web proxy in front of Nginx Unit.

3. Install and configure Nginx with Let's Encrypt

Let's start by installing the Nginx webserver:

# apt install nginx

To configure Nginx, we will define an upstream receiving the requests from the Nginx web server. We also define a /static/ to indicate the Django static directory.

Here is the Nginx configuration you can put in /etc/nginx/conf.d:

upstream unit_backend {
 server 127.0.0.1:8300;
}

server {
 listen 80;
 server_name myapp.com;
 return 301 https://myapp.com$request_uri;
}

server {
 listen 443 ssl;
 ssl_certificate /etc/letsencrypt/live/myapp.com/fullchain.pem;
 ssl_certificate_key /etc/letsencrypt/live/myapp.com/privkey.pem;

server_name myapp.com;
 access_log /var/log/nginx/myapp.com.access.log;
 error_log /var/log/nginx/myapp.error.log;

root /home/myapp/prod/myapp;

location = /favicon.ico { access_log off; log_not_found off; }
 location /static {
 root /home/myapps/prod/myapp;
 }

location / {
 proxy_pass http://unit_backend;
 proxy_set_header Host $host;
 }
 location /.well-known {
 allow all;
 }
}

Before starting Nginx (stop it if it is running), we'll get our SSL certificate from Let's Encrypt.

# certbot certonly -d myapp.com

Spin a temporary web server and get your certificate.

Now we're almost ready. Start the Nginx web server:

# systemctl start nginx

4. Configure Django for production

Your Django settings file, here the /home/myapp/prod/myapp/myapp/settings.py file should use paths existing on your server e.g you should have the following STATIC_ROOT in the settings.py of your app:

STATIC_ROOT = '/home/myapp/prod/myapp/static/'

Pitfall here: the root in the Nginx configuration for the static we wrote above is one level upper: /home/myapp/prod/myapp Use the correct path or your static won't appear.

Just a last step for Django: at the root of your Django app, you need to collect the static files in the dedicated directory with the following command:

$ python3 manage.py collectstatic

Conclusion

This setup runs in production. Except two pitfalls, it's quite straightforward to setup. If you encounter any error, please write a comment below and I'll fix the article.

About Me

Carl Chenet, Free Software Indie Hacker, Founder of LinuxJobs.fr, a job board for Free and Open Source Jobs in France.

Follow Me On Social Networks

24 Apr 2018 10:00pm GMT

Olivier Berger: Added docker container to my org-teaching framework to ease org-mode exports

I've improved a bit the org-teaching framework in order to prepare for the next edition of the CSC4101 classes.

I've now added a docker container which is in charge of performing the HTML or PDF exports of the slides (using org-reveal) or handbooks (using LaTeX).

Emacs and org-mode are still advised for editing contents, but having this container in the loop ensures that colleagues are able to preview the changes to the teaching material, and I'm no longer a bottleneck for generating the handouts. This also allows to export in a reproducible way, which doesn't depend on my Emacs config tweaks.

I've also added Gitlab pages to the project's CI so that the docs are updated live at https://olberger.gitlab.io/org-teaching/.

It's probably not yet rady for use by anyone else, but I'd be glad to get feedback 😉

24 Apr 2018 11:13am GMT

Reproducible builds folks: Reproducible Builds: Weekly report #156

Here's what happened in the Reproducible Builds effort between Sunday April 15 and Saturday April 21 2018:

Packages reviewed and fixed, and bugs filed

In addition, Chris Lamb's patch to the Freeland VPN client was merged upstream and build failure bugs were reported by Adrian Bunk (48), Paul Gevers (5) and Rafael Laboissière (1).

jenkins.debian.net development

A large number of changes were made to our Jenkins-based testing framework, including:

Reviews of unreproducible packages

43 package reviews have been added, 49 have been updated and 97 have been removed in this week, adding to our knowledge about identified issues.

One new issue was added by Chris Lamb: build_path_in_index_files_generated_by_qdoc. In addition, three issue types were removed (random_ispell_hash_files, randomness_in_python_setuptools_pkg_info & timestamps_in_documentation_generated_by_asciidoctora) and one was updated (timestamp_in_pear_registry_files).

Misc.

This week's edition was written by Bernhard M. Wiedemann, Chris Lamb, Holger Levsen & reviewed by a bunch of Reproducible Builds folks on IRC & the mailing lists.

24 Apr 2018 6:16am GMT

Holger Levsen: 20180423-technohippieparadise

Trouble in techno hippie paradise

So I'm in some 'jungle' in Brasil, enjoying a good time with some friends which another friend jokingly labeled as cryptohippies, enjoying the silence, nature, good food, some cats & dogs and 3g internet. Life is good here.

And then we decided to watch "Stare into the lights my pretties" and while it is a very good and insightful movie, it's also disturbing to see just how much we, as human societies, have changed ourselves mindlessly (or rather, out of our own minds) in very recent history.

Even though not a smartphone user myself and while seemingly aware and critical of many changes happening in the last two decades, the movie was still eyeopening to me. Now if there only werent 100 distractions per day I would maybe be able to build up on this. Or maybe I need to watch it every week, though this wouldn't work neither, as the movie explains so well...

The movie also reminded me why I dislike being cc:ed on email so much (unless urgent and when I'm subscribed to the list being posted to). Because usually during the day I (try to) ignore list mails, but I do check my personal inboxes. And if someone cc:s me, this breaks my lines of thoughts. So it seems I still need to get better at ignoring stuff, even if something is pushed to me. Maybe especially then. (And hints for good .procmail rules for this much appreciated.)

Another interesting point: while the number of people addicted to nicotine has been going down globally lately, the number of network addicts has outnumbered those by far now. And yet the long term effects of being online almost 24/365 have not yet been researched at all. The cigarette companies claimed that most doctors smoke. The IT industry claims it's normal to be online. What's your wakeup2smartphone time? Do you check email every day?

This movie also made me wonder what Debian's role will, can and should be in this future. (And where of course I don't only mean Debian, but free software, free societies, in general.)

So, this movie brings up many questions. (And nicely explains why people rather don't like that.) So go watch this movie! You will be touched, think and check your email/smartphone afterwards.

(And finally, of course it's ironic that the movie is on youtube. And so I learned that to download subtitles you need to tell youtube-dl so, and it's easiest by using --all-subs. And btw, youtube-dl-gui needs help with running with python3 and thus with getting into Debian.)

24 Apr 2018 12:25am GMT

23 Apr 2018

feedPlanet Debian

Benjamin Mako Hill: Is English Wikipedia’s ‘rise and decline’ typical?

This graph shows the number of people contributing to Wikipedia over time:

The Rise and Decline of Wikipedia The number of active Wikipedia contributors exploded, suddenly stalled, and then began gradually declining. (Figure taken from Halfaker et al. 2013)

The figure comes from "The Rise and Decline of an Open Collaboration System," a well-known 2013 paper that argued that Wikipedia's transition from rapid growth to slow decline in 2007 was driven by an increase in quality control systems. Although many people have treated the paper's finding as representative of broader patterns in online communities, Wikipedia is a very unusual community in many respects. Do other online communities follow Wikipedia's pattern of rise and decline? Does increased use of quality control systems coincide with community decline elsewhere?

In a paper that my student Nathan TeBlunthuis is presenting Thursday morning at the Association for Computing Machinery (ACM) Conference on Human Factors in Computing Systems (CHI), a group of us have replicated and extended the 2013 paper's analysis in 769 other large wikis. We find that the dynamics observed in Wikipedia are a strikingly good description of the average Wikia wiki. They appear to reoccur again and again in many communities.

The original "Rise and Decline" paper (we'll abbreviate it "RAD") was written by Aaron Halfaker, R. Stuart Geiger, Jonathan T. Morgan, and John Riedl. They analyzed data from English Wikipedia and found that Wikipedia's transition from rise to decline was accompanied by increasing rates of newcomer rejection as well as the growth of bots and algorithmic quality control tools. They also showed that newcomers whose contributions were rejected were less likely to continue editing and that community policies and norms became more difficult to change over time, especially for newer editors.

Our paper, just published in the CHI 2018 proceedings, replicates most of RAD's analysis on a dataset of 769 of the largest wikis from Wikia that were active between 2002 to 2010. We find that RAD's findings generalize to this large and diverse sample of communities.

We can walk you through some of the key findings. First, the growth trajectory of the average wiki in our sample is similar to that of English Wikipedia. As shown in the figure below, an initial period of growth stabilizes and leads to decline several years later.

Rise and Decline on Wikia The average Wikia wikia also experience a period of growth followed by stabilization and decline (from TeBlunthuis, Shaw, and Hill 2018).

We also found that newcomers on Wikia wikis were reverted more and continued editing less. As on Wikipedia, the two processes were related. Similar to RAD, we also found that newer editors were more likely to have their contributions to the "project namespace" (where policy pages are located) undone as wikis got older. Indeed, the specific estimates from our statistical models are very similar to RAD's for most of these findings!

There were some parts of the RAD analysis that we couldn't reproduce in our context. For example, there are not enough bots or algorithmic editing tools in Wikia to support statistical claims about their effects on newcomers.

At the same time, we were able to do some things that the RAD authors could not. Most importantly, our findings discount some Wikipedia-specific explanations for a rise and decline. For example, English Wikipedia's decline coincided with the rise of Facebook, smartphones, and other social media platforms. In theory, any of these factors could have caused the decline. Because the wikis in our sample experienced rises and declines at similar points in their life-cycle but at different points in time, the rise and decline findings we report seem unlikely to be caused by underlying temporal trends.

The big communities we study seem to have consistent "life cycles" where stabilization and/or decay follows an initial period of growth. The fact that the same kinds of patterns happen on English Wikipedia and other online groups implies a more general set of social dynamics at work that we do not think existing research (including ours) explains in a satisfying way. What drives the rise and decline of communities more generally? Our findings make it clear that this is a big, important question that deserves more attention.

We hope you'll read the paper and get in touch by commenting on this post or emailing Nate if you'd like to learn or talk more. The paper is available online and has been published under an open access license. If you really want to get into the weeds of the analysis, we will soon publish all the data and code necessary to reproduce our work in a repository on the Harvard Dataverse.

Nate TeBlunthuis will be presenting the project this week at CHI in Montréal on Thursday April 26 at 9am in room 517D. For those of you not familiar with CHI, it is the top venue for Human-Computer Interaction. All CHI submissions go through double-blind peer review and the papers that make it into the proceedings are considered published (same as journal articles in most other scientific fields). Please feel free to cite our paper and send it around to your friends!

This blog post, and the open access paper that it describes, is a collaborative project with Aaron Shaw, that was led by Nate TeBlunthuis. A version of this blog post was originally posted on the Community Data Science Collective blog. Financial support came from the US National Science Foundation (grants IIS-1617129, IIS-1617468, and GRFP-2016220885 ), Northwestern University, the Center for Advanced Study in the Behavioral Sciences at Stanford University, and the University of Washington. This project was completed using the Hyak high performance computing cluster at the University of Washington.

23 Apr 2018 9:20pm GMT

Vincent Bernat: A more privacy-friendly blog

When I started this blog, I embraced some free services, like Disqus or Google Analytics. These services are quite invasive for users' privacy. Over the years, I have tried to correct this to reach a point where I do not rely on any "privacy-hostile" services.

Analytics🔗

Google Analytics is an ubiquitous solution to get a powerful analytics solution for free. It's also a great way to provide data about your visitors to Google-also for free. There are self-hosted solutions like Matomo-previously Piwik.

I opted for a simpler solution: no analytics. It also enables me to think that my blog attracts thousands of visitors every day.

Fonts🔗

Google Fonts is a very popular font library and hosting service, which relies on the generic Google Privacy Policy. The google-webfonts-helper service makes it easy to self-host any font from Google Fonts. Moreover, with help from pyftsubset, I include only the characters used in this blog. The font files are lighter and more complete: no problem spelling "Antonín Dvořák".

Videos🔗

Some articles are supported by a video (like "OPL2LPT: an AdLib sound card for the parallel port"). In the past, I was using YouTube, mostly because it was the only free platform with an option to disable ads. Streaming on-demand videos is usually deemed quite difficult. For example, if you just use the <video> tag, you may push a too big video for people with a slow connection. However, it is not that hard, thanks to hls.js, which enables to deliver video sliced in segments available at different bitrates. Users with Java­Script disabled are still delivered with a progressive version of medium quality.

In "Self-hosted videos with HLS", I explain this approach in more details.

Comments🔗

Disqus is a popular comment solution for static websites. They were recently acquired by Zeta Global, a marketing company and their business model is supported only by advertisements. On the technical side, Disqus also loads several hundred kilobytes of resources. Therefore, many websites load Disqus on demand. That's what I did. This doesn't solve the privacy problem and I had the sentiment people were less eager to leave a comment if they had to execute an additional action.

For some time, I thought about implementing my own comment system around Atom feeds. Each page would get its own feed of comments. A piece of Java­Script would turn these feeds into HTML and comments could still be read without Java­Script, thanks to the default rendering provided by browsers. People could also subscribe to these feeds: no need for mail notifications! The feeds would be served as static files and updated on new comments by a small piece of server-side code. Again, this could work without Javascript.

Day Planner by Fowl Language Comics

Fowl Language Comics: Day Planner or the real reason why I didn't code a new comment system.

I still think this is a great idea. But I didn't feel like developing and maintaining a new comment system. There are several self-hosted alternatives, notably Isso and Commento. Isso is a bit more featureful, with notably an imperfect import from Disqus. Both are struggling with maintenance and are trying to become sustainable with a paid hosted version.1 Commento is more privacy-friendly as it doesn't use cookies at all. However, cookies from Isso are not essential and can be filtered with nginx:

proxy_hide_header Set-Cookie;
proxy_hide_header X-Set-Cookie;
proxy_ignore_headers Set-Cookie;

In Isso, there is currently no mail notifications, but I have added an Atom feed for each comment thread.

Another option would have been to not provide comments anymore. However, I had some great contributions as comments in the past and I also think they can work as some kind of peer review for blog articles: they are a weak guarantee that the content is not totally wrong.

Search engine🔗

A way to provide a search engine for a personal blog is to provide a form for a public search engine, like Google. That's what I did. I also slapped some Java­Script on top of that to make it look like not Google.

The solution here is easy: switch to DuckDuckGo, which lets you customize a bit the search experience:

<form id="lf-search" action="https://duckduckgo.com/">
  <input type="hidden" name="kf" value="-1">
  <input type="hidden" name="kaf" value="1">
  <input type="hidden" name="k1" value="-1">
  <input type="hidden" name="sites" value="vincent.bernat.im/en">
  <input type="submit" value="">
  <input type="text" name="q" value="" autocomplete="off" aria-label="Search">
</form>

The Java­Script part is also removed as DuckDuckGo doesn't provide an API. As it is unlikely that more than three people will use the search engine in a year, this seems a good idea to not spend too much time on this non-essential feature.

Newsletter🔗

Nowadays, RSS feeds are far less popular they were before. I am still baffled as why a technical audience wouldn't use RSS, but some readers prefer to receive updates by mail.

MailChimp is a common solution to send newsletters. It provides a simple integration with RSS feeds to trigger a mail each time new items are added to the feed. From a privacy point of view, MailChimp seems a good citizen: data collection is mainly limited to the amount needed to operate the service. Privacy-conscious users can still avoid this service and use the RSS feed.

Less Java­Script🔗

Many privacy-conscious people are disabling Java­Script or using extensions like uMatrix or NoScript. Except for comments, I was using Java­Script only for non-essential stuff:

For mathematical formulae, I have switched from MathJax to KaTeX. The later is faster but also enables server-side rendering: it produces the same output regardless of browser. Therefore, client-side Java­Script is not needed anymore.

For sidenotes, I have turned the Java­Script code doing the transformation into Python code, with pyquery. No more client-side Java­Script for this aspect either.

The remaining code is still here but is self-hosted.

Memento: CSP🔗

The HTTP Content-Security-Policy header controls the resources that a user agent is allowed to load for a given page. It is a safeguard and a memento for the external resources a site will use. Mine is moderately complex and shows what to expect from a privacy point of view:3

Content-Security-Policy:
  default-src 'self' blob:;
  script-src  'self' blob: https://d1g3mdmxf8zbo9.cloudfront.net/js/;
  object-src  'self' https://d1g3mdmxf8zbo9.cloudfront.net/images/;
  img-src     'self' data: https://d1g3mdmxf8zbo9.cloudfront.net/images/;
  frame-src   https://d1g3mdmxf8zbo9.cloudfront.net/images/;
  style-src   'self' 'unsafe-inline' https://d1g3mdmxf8zbo9.cloudfront.net/css/;
  font-src    'self' about: data: https://d1g3mdmxf8zbo9.cloudfront.net/fonts/;
  worker-src  blob:;
  media-src   'self' blob: https://luffy-video.sos-ch-dk-2.exo.io;
  connect-src 'self' https://luffy-video.sos-ch-dk-2.exo.io https://comments.luffy.cx;
  frame-ancestors 'none';
  block-all-mixed-content;

I am quite happy having been able to reach this result. 😊

  1. For Isso, look at comment.sh. For Commento, look at commento.io. ↩︎

  2. You may have noticed I am a footnote sicko and use them all the time for pointless stuff. ↩︎

  3. I don't have issue with using a CDN like CloudFront: it is a paid service and Amazon AWS is not in the business of tracking users. ↩︎

23 Apr 2018 8:01am GMT

22 Apr 2018

feedPlanet Debian

Joachim Breitner: Verifying local definitions in Coq

TL;DR: We can give top-level names to local definitions, so that we can state and prove stuff about them without having to rewrite the programs.

When a Haskeller writes Coq

Imagine you teach Coq to a Haskell programmer, and give them the task of pairing each element in a list with its index. The Haskell programmer might have

addIndex :: [a] -> [(Integer, a)]
addIndex xs = go 0 xs
  where go n [] = []
        go n (x:xs) = (n,x) : go (n+1) xs

in mind and write this Gallina function (Gallina is the programming language of Coq):

Require Import Coq.Lists.List.
Import ListNotations.

Definition addIndex {a} (xs : list a) : list (nat * a) :=
  let fix go n xs := match xs with
                     | []    => []
                     | x::xs => (n, x) :: go (S n) xs
                     end
  in go 0 xs.

Alternatively, imagine you are using hs-to-coq to mechanically convert the Haskell definition into Coq.

When a Coq user tries to verify that

Now your task is to prove something about this function, for example

Theorem addIndex_spec:
  forall {a} n (xs : list a),
  nth n (map fst (addIndex xs)) n = n.

If you just have learned Coq, you will think "I can do this, this surely holds by induction on xs." But if you have a bit more experience, you will already see a problem with this (if you do not see the problem yet, I encourage you to stop reading, copy the few lines above, and try to prove it).

The problem is that - as so often - you have to generalize the statement for the induction to go through. The theorem as stated says something about addIndex or, in other words, about go 0. But in the inductive case, you will need some information about go 1. In fact, you need a lemma like this:

Lemma go_spec:
  forall {a} n m k (xs : list a), k = n + m ->
  nth n (map fst (go m xs)) k = k.

But go is not a (top-level) function! How can we fix that?

The weird trick

We can define go after-the-fact, but instead of copy'n'pasting the definition, we can use Coq's tactics to define it. Here it goes:

Definition go {a} := ltac:(
  let e := eval cbv beta delta [addIndex] in (@addIndex a []) in
  (* idtac e; *)
  lazymatch e with | let x := ?def in _ =>
    exact def
  end).

Let us take it apart:

  1. We define go, and give the parameters that go depends upon. Note that of the two parameters of addIndex, the definition of go only depends on ("captures") a, but not xs.
  2. We do not give a type to go. We could, but that would again just be copying information that is already there.
  3. We define go via an ltac expression: Instead of a term we give a tactic that calculates the term.
  4. This tactic first binds e to the body of addIndex. To do so, it needs to pass enough arguments to addIndex. The concrete value of the list argument does not matter, so we pass []. The term @addIndex a [] is now evaluated with the evaluation flags eval cbv beta delta [addIndex], which says "unfold addIndex and do beta reduction, but nothing else". In particularly, we do not do zeta reduction, which would reduce the let go := … definition. (The user manual very briefly describes these flags.)
  5. The idtac e line can be used to peek at e, for example when the next tactic fails. We can use this to check that e really is of the form let fix go := … in ….
  6. The lazymatch line matches e against the pattern let x := ?def in _, and binds the definition of go to the name def.
  7. And the exact def tactic tells Coq to use def as the definition of go.

We now have defined go, of type go : forall {a}, nat -> list a -> list (nat * a), and can state and prove the auxiliary lemma:

Lemma go_spec:
  forall {a} n m k (xs : list a), k = n + m ->
  nth n (map fst (go m xs)) k = k.
Proof.
  intros ?????.
  revert n m k.
  induction xs; intros; destruct n; subst; simpl.
  1-3:reflexivity.
  apply IHxs; lia.
Qed.

When we come to the theorem about addIndex, we can play a little trick with fold to make the proof goal pretty:

Theorem addIndex_spec:
  forall {a} n (xs : list a),
  nth n (map fst (addIndex xs)) n = n.
Proof.
  intros.
  unfold addIndex.
  fold (@go a).
  (* goal here: nth n (map fst (go 0 xs)) n = n *)
  apply go_spec; lia.
Qed.

Multiple local definitions

The trick extends to multiple local definitions, but needs some extra considerations to ensure that terms are closed. A bit contrived, but let us assume that we have this function definition:

Definition addIndex' {a} (xs : list a) : list (nat * a) :=
  let inc := length xs in
  let fix go n xs := match xs with
                     | []    => []
                     | x::xs => (n, x) :: go (inc + n) xs
                     end in
  go 0 xs.

We now want to give names to inc and to go. I like to use a section to collect the common parameters, but that is not essential here. The trick above works flawlessly for `inc':

Section addIndex'.
Context {a} (xs : list a).

Definition inc := ltac:(
  let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
  lazymatch e with | let x := ?def in _ =>
    exact def
  end).

But if we try it for go', like such:

Definition go' := ltac:(
  let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
  lazymatch e with | let x := _ in let y := ?def in _ =>
    exact def
  end).

we get "Ltac variable def depends on pattern variable name x which is not bound in current context". To fix this, we use higher-order pattern matchin (@?def) to substitute "our" inc for the local inc:

Definition go' := ltac:(
  let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
  lazymatch e with | let x := _ in let y := @?def x in _ =>
    let def' := eval cbv beta in (def inc) in
    exact def'
  end).

instead. We have now defined both inc and go' and can use them in proofs about addIndex':

Theorem addIndex_spec':
  forall n, nth n (map fst (addIndex' xs)) n = n * length xs.
Proof.
  intros.
  unfold addIndex'.
  fold inc go'. (* order matters! *)
  (* goal here: nth n (map fst (go' 0 xs)) n = n * inc *)

Reaching into a match

This trick also works when the local definition we care about is inside a match statement. Consider:

Definition addIndex_weird {a} (oxs : option (list a))
  := match oxs with
     | None => []
     | Some xs =>
       let fix go n xs := match xs with
                          | []    => []
                          | x::xs => (n, x) :: go (S n) xs
                          end in
       go 0 xs
     end.

Definition go_weird {a} := ltac:(
  let e := eval cbv beta match delta [addIndex_weird]
           in (@addIndex_weird a (Some [])) in
  idtac e;
  lazymatch e with | let x := ?def in _ =>
    exact def
  end).

Note the addition of match to the list of evaluation flags passed to cbv.

Conclusion

While local definitions are idiomatic in Haskell (in particular thanks to the where syntax), they are usually avoided in Coq, because they get in the way of verification. If, for some reason, one is stuck with such definitions, then this trick presents a reasonable way out.

22 Apr 2018 9:47pm GMT

Sam Hartman: Shaving the DJ Software Yak

I'm getting married this June. (For the Debian folks, the Ghillie shirt and vest just arrived to go with the kilt. My thanks go out to the lunch table at Debconf that made that suggestion. formal Scottish dress would not have fit, but I wanted something to go with the kilt.)
Music and dance have been an important part of my spiritual journey. Dance has also been an import part of the best weddings I attended. So I wanted dance to be a special part of our celebration. I put together a play list for my 40th birthday; it was special and helped set the mood for the event. Unfortunately, as I started looking at what I wanted to play for the wedding, I realized I needed to do better. Some of the songs were too long. Some of them really felt like they needed a transition. I wanted a continuous mix not a play list.
I'm blind. I certainly could use two turn tables and a mixer--or at least I could learn how to do so. However, I'm a kid of the electronic generation, and that's not my style. So, I started looking at DJ software. With one exception, everything I found was too visual for me to use.
I've used Nama before to put together a mashup. It seemed like Nama offered almost everything I needed. Unfortunately, there were a couple of problems. Nama would not be a great fit for a live mix: you cannot add tracks or effects into the chain without restarting the engine. I didn't strictly need live production for this project, but I wanted to look at that long-term. At the time of my analysis, I thought that Nama didn't support tempo-scaling tracks. For that reason, I decided I was going to have to write my own software. Later I learned that you can adjust the sample rate on a track import, which is more or less good enough for tempo scaling. By that point I already had working code.
I wanted a command line interface. I wanted BPM and key detection; it looked like Mixxx was open-source software with good support for that. Based on my previous work, I chose Csound as the realtime sound backend.

Where I got


I'm proud of what I came up with. I managed to stay focused on my art rather than falling into the trap of focusing too much on the software. I got something that allows me to quickly explore the music I want to mix, but also managed to accomplish my goal and come up with a mix that I'm really happy with. As a result, at the current time, my software is probably only useful to me. However, it is available under the GPL V3. If anyone else would be interested in hacking on it, I'd be happy to spend some time documenting and working with them.
Here's a basic description of the approach.


There's some preliminary support for a MIDI controller I was given, but I realized that coding that wasn't actually going to save me time, so I left it. This was a really fun project. I managed to tell a story for my wedding that is really important for me to tell. I learned a lot about what goes into putting together a mix. It's amazing how many decisions go into even simple things like a pan slider. It was also great that there is free software for me to build on top of. I got to focus on the part of the problem I wanted to solve. I was able to reuse components for the realtime sound work and for analysis like BPM detection.

22 Apr 2018 8:55pm GMT

Wouter Verhelst: host detection in bash

There are many tools to implement this, and yeah, this is not the fastest. But the advantage is that you don't need extra tools beyond "bash" and "ping"...

for i in $(seq 1 254); do
  if ping -W 1 -c 1 192.168.0.$i; then
    HOST[$i]=1
  fi
done
echo ${!HOST[@]}

will give you the host addresses for the machines that are live on a given network...

22 Apr 2018 10:04am GMT

Norbert Preining: Specification and Verification of Software with CafeOBJ – Part 2 – Basics of CafeOBJ

This blog continues Part 1 of our series on software specification and verification with CafeOBJ.

Availability of CafeOBJ

CafeOBJ can be obtained from the website cafeobj.org. The site provides binary packages built from Linux, MacOS, and Windows, as well as the source code for those who want to build the interpreter themselves. Other services provided are tutorial pages, all kind of documentation (reference manual, wiki, user manual).

What is CafeOBJ

Let us recall some of the items mentioned in the previous blog. CafeOBJ is an algebraic specification language, as well as a verification and programming language. This means, that specifications written in CafeOBJ can be verified right within the system without the need to regress to external utilities.

As algebraic specification language it is built upon the logical foundation formed by the following items: (i) order sorted algebras, (ii) co-algebras (or hidden algebras), and (iii) rewriting logic. As verification and programming language it provides the user with an executable semantics of the equational theory, a rewrite engine that supports conditional, order-sorted, AC (associative and commutative) rewriting, a sofisticated module system including parametrization and inheritance, and last but not least a completely free syntax.

The algebraic semantics can be represented by the CafeOBJ cube exhibiting the various extensions starting more many sorted algebras:

For the algebraically inclined audience we just mention that all the systems and morphisms are formalized as institutions and institution morphisms.

Let us now go through some the the logical foundations of CafeOBJ:

Term rewriting

Term rewriting is concerned with systems of rules to replace certain parts of an expression with another expression. A very simple example of a rewrite system is:

  append(nil, ys)    → ys
  append(x : xs, ys) → x : append(xs, ys)

Here the first rule says that you can rewrite an expression append(nil, ys) where ys can be any list, with ys itself. And the second rule states how to rewrite an expression when the first element is not the empty list.

A typical reduction sequence - that is application of these rules - would be:

append(1 ∶ 2 ∶ 3 ∶ nil, 4 ∶ 5 ∶ nil) → 1 ∶ append(2 ∶ 3 ∶ nil, 4 ∶ 5 ∶ nil)
                                     → 1 ∶ 2 ∶ append(3 ∶ nil, 4 ∶ 5 ∶ nil)
                                     → 1 ∶ 2 ∶ 3 ∶ append(nil, 4 ∶ 5 ∶ nil)
                                     → 1 ∶ 2 ∶ 3 ∶ 4 ∶ 5 ∶ nil

Term rewriting is used in two different ways in CafeOBJ: First as execution engine that considers equations as directed rules and uses them to reduce expressions. And at the same time rewriting logic is included into the language specification allowing for reasoning about transitions.

Order sorted algebras

Most algebras we learn in school or even at the university are single sorted, that is all objects in the algebra are of the same type (e.g., integers, reals, function space). In this case an operation is determined by its arity, that is the number of arguments.

In the many sorted and order sorted case the simple number of arguments of a function is not enough, we need to know for each argument its type and also the type of the value the function returns. Thus, we assume a signature (S,F) given, such that S is a set of sorts, or simply sort names, and F is a set of operations f: s1, s2, ..., sk → s where all the s are sorts.

As an example assume we have two sorts, String and Int, one possible function would be

  substr: String, Int, Int → String

which would tell us that the function substr takes three arguments, the first of sort String, the others of sort Int, and it returns again a value of sort String.

In case the sorts are (partially ordered), we call the corresponding algebra order sorted algebra.

Using order sorted algebras has several advantages compared to other algebraic systems:

We want to close this blog post with a short history of CafeOBJ and a short sample list of specifications that have been carried out with CafeOBJ.

History, background, relatives, and examples

CafeOBJ, as an algebraic specification language based on equational theory, has its roots in CLEAR (Burgstall and Goguen, early 70s) and the OBJ language (Goguen et al, 70-80s SRI and UC San Diego). The successor OBJ2 was developed by Futatsugi, Goguen, Jouannaud, and Meseguer at UC San Diego in 1984, based on Horn logic, sub-sorts, and parametrized modules.

The developer then moved on to different languages or extensions: Meseguer started to develop Maude, Jouannaud moved on to develop Coq, an unrelated language, and Futatsugi built upon the OBJ3 language by Kirchner et al to create CafeOBJ.

Example specifications carried out in CafeOBJ are authentication protocols (NSLPK, STS, Otway-Rees), key secrecy PACE protocol (German passport), e-commerce protocols (SET), real time algorithms (Fischer's mutual exclusion protocol), UML semantics, formal fault tree analysis.

In the next blog post we will make first steps with the CafeOBJ interpreter and see how to define modules, the basic building blocks, and carry out simple computations.

22 Apr 2018 2:47am GMT

21 Apr 2018

feedPlanet Debian

Benjamin Mako Hill: Mako Hate

I recently discovered a prolific and sustained community of meme-makers on Tumblr dedicated to expressing their strong dislike for "Mako."

Two tags with examples are #mako hate and #anti mako but there are many others.

I've also discovered Tumblrs entirely dedicated to the topic!

For example, Let's Roast Mako describes itself "A place to beat up Mako. In peace. It's an inspiration to everyone!"

The second is the Fuck Mako Blog which describes itself with series of tag-lines including "Mako can fuck right off and we're really not sorry about that," "Welcome aboard the SS Fuck-Mako;" and "Because Mako is unnecessary." Sub-pages of the site include:

I'll admit I'm a little disquieted.

21 Apr 2018 9:31pm GMT

Joey Hess: my haskell controlled offgrid fridge

I'm preparing for a fridge upgrade, away from the tiny propane fridge to a chest freezer conversion. My home computer will be monitoring the fridge temperature and the state of my offgrid energy system, and turning the fridge on and off using a relay and the inverter control board I built earlier.

This kind of automation is a perfect fit for Functional Reactive Programming (FRP) since it's all about time-varying behaviors and events being combined together.

Of course, I want the control code to be as robust as possible, well tested, and easy to modify without making mistakes. Pure functional Haskell code.

There are many Haskell libraries for FRP, and I have not looked at most of them in any detail. I settled on reactive-banana because it has a good reputation and amazing testimonials.

"In the programming-language world, one rule of survival is simple: dance or die. This library makes dancing easy." - Simon Banana Jones

But, it's mostly used for GUI programming, or maybe some musical live-coding. There were no libraries for using reactive-banana for the more staid task of home automation, or anything like that. Also, using it involves a whole lot of IO code, so not great for testing.

So I built reactive-banana-automation on top of it to address my needs. I think it's a pretty good library, although I don't have a deep enough grokking of FRP to say that for sure.

Anyway, it's plenty flexible for my fridge automation needs, and I also wrote a motion-controlled light automation with it to make sure it could be used for something else (and to partly tackle the problem of using real-world time events when the underlying FRP library uses its own notion of time).

The code for my fridge is a work in progress since the fridge has not arrived yet, and because the question of in which situations an offgrid fridge should optimally run and not run is really rather complicated.

Here's a simpler example, for a non-offgrid fridge.

fridge :: Automation Sensors Actuators
fridge sensors actuators = do
        -- Create a Behavior that reflects the most recently reported
        -- temperature of the fridge.
        btemperature <- sensedBehavior (fridgeTemperature sensors)
        -- Calculate when the fridge should turn on and off.
        let bpowerchange = calcpowerchange <$> btemperature
        onBehaviorChangeMaybe bpowerchange (actuators . FridgePower)
  where
        calcpowerchange (Sensed temp)
                | temp `belowRange` allowedtemp = Just PowerOff
                | temp `aboveRange` allowedtemp = Just PowerOn
                | otherwise = Nothing
        calcpowerchange SensorUnavailable = Nothing
        allowedtemp = Range 1 4

And here the code is being tested in a reproducible fashion:

> runner <- observeAutomation fridge mkSensors
> runner $ \sensors -> fridgeTemperature sensors =: 6
[FridgePower PowerOn]
> runner $ \sensors -> fridgeTemperature sensors =: 3
[]
> runner $ \sensors -> fridgeTemperature sensors =: 0.5
[FridgePower PowerOff]

BTW, building a 400 line library and writing reams of control code for a fridge that has not been installed yet is what we Haskell programmers call "laziness".

21 Apr 2018 8:45pm GMT

Lisandro Damián Nicanor Pérez Meyer: moving Qt 4 from Debian testing (aka Buster): some statistics, update II

As in my previous blogpost I'm taking a look at our Qt4 removal wiki page.

Of a total of 438 filed bugs:

We started filing bugs around September 9. That means roughly 32 weeks which gives us around 5.65 packages fixed per week, aka 0.85 packages per day. Obviously not as good as we started (remaining bugs tend to be more complicated), but still quite good.

So, how can you help?

If you are a maintainer of any of the packages still affected try to get upstream to make a port and package it.

If you are not a maintainer you might want to take a look at the list of packages in our wiki page and try to create a patch for them. If you can submit it directly to upstream, the better. Or maybe it's time for you to become the package's upstream or maintainer!



21 Apr 2018 12:47pm GMT

Vincent Bernat: OPL2 Audio Board: an AdLib sound card for Arduino

In a previous article, I presented the OPL2LPT, a sound card for the parallel port featuring a Yamaha YM3812 chip, also known as OPL2-the chip of the AdLib sound card. The OPL2 Audio Board for Arduino is another indie sound card using this chip. However, instead of relying on a parallel port, it uses a serial interface, which can be drived from an Arduino board or a Raspberry Pi. While the OPL2LPT targets retrogamers with real hardware, the OPL2 Audio Board cannot be used in the same way. Nonetheless, it can also be operated from ScummVM and DOSBox!

OPL2 Audio Board for Arduino

The OPL2 Audio Board over a "Grim Fandango" box.

Unboxing🔗

The OPL2 Audio Board can be purchased on Tindie, either as a kit or fully assembled. I have paired it with a cheap clone of the Arduino Nano. A library to drive the board is available on GitHub, along with some examples.

One of them is DemoTune.ino. It plays a short tune on three channels. It can be compiled and uploaded to the Arduino with PlatformIO-installable with pip install platformio-using the following command:1

$ platformio ci \
    --board nanoatmega328 \
    --lib ../../src \
    --project-option="targets=upload" \
    --project-option="upload_port=/dev/ttyUSB0" \
    DemoTune.ino
[...]
PLATFORM: Atmel AVR > Arduino Nano ATmega328
SYSTEM: ATMEGA328P 16MHz 2KB RAM (30KB Flash)
Converting DemoTune.ino
[...]
Configuring upload protocol...
AVAILABLE: arduino
CURRENT: upload_protocol = arduino
Looking for upload port...
Use manually specified: /dev/ttyUSB0
Uploading .pioenvs/nanoatmega328/firmware.hex
[...]
avrdude: 6618 bytes of flash written
[...]
===== [SUCCESS] Took 5.94 seconds =====

Immediately after the upload, the Arduino plays the tune. 🎶

The next interesting example is SerialIface.ino. It turns the audio board into a sound card over serial port. Once the code has been pushed to the Arduino, you can use the play.py program in the same directory to play VGM files. They are a sample-accurate sound format for many sound chips. They log the exact commands sent. There are many of them on VGMRips. Be sure to choose the ones for the YM3812/OPL2! Here is a small selection:

The OPL2 Audio Board playing some VGM files. It is connected to an Arduino Nano. You can see the LEDs blinking when the Arduino receives the commands from the serial port.

Usage with DOSBox & ScummVM🔗

Notice

The support for the serial protocol used in this section has not been merged yet. In the meantime, grab SerialIface.ino from the pull request: git checkout 50e1717.

When the Arduino is flashed with SerialIface.ino, the board can be driven through a simple protocol over the serial port. By patching DOSBox and ScummVM, we can make them use this unusual sound card. Here are some examples of games:

DOSBox🔗

The serial protocol is described in the SerialIface.ino file:

/*
 * A very simple serial protocol is used.
 *
 * - Initial 3-way handshake to overcome reset delay / serial noise issues.
 * - 5-byte binary commands to write registers.
 *   - (uint8)  OPL2 register address
 *   - (uint8)  OPL2 register data
 *   - (int16)  delay (milliseconds); negative -> pre-delay; positive -> post-delay
 *   - (uint8)  delay (microseconds / 4)
 *
 * Example session:
 *
 * Arduino: HLO!
 * PC:      BUF?
 * Arduino: 256 (switches to binary mode)
 * PC:      0xb80a014f02 (write OPL register and delay)
 * Arduino: k
 *
 * A variant of this protocol is available without the delays. In this
 * case, the BUF? command should be sent as B0F? The binary protocol
 * is now using 2-byte binary commands:
 *   - (uint8)  OPL2 register address
 *   - (uint8)  OPL2 register data
 */

Adding support for this protocol in DOSBox is relatively simple (patch). For best performance, we use the 2-byte variant (5000 ops/s). The binary commands are pipelined and a dedicated thread collects the acknowledgments. A semaphore captures the number of free slots in the receive buffer. As it is not possible to read registers, we rely on DOSBox to emulate the timers, which are mostly used to let the various games detect the OPL2.

The patch is tested only on Linux but should work on any POSIX system-not Windows. To test it, you need to build DOSBox from source:

$ sudo apt build-dep dosbox
$ git clone https://github.com/vincentbernat/dosbox.git -b feature/opl2audioboard
$ cd dosbox
$ ./autogen.sh
$ ./configure && make

Replace the sblaster section of ~/.dosbox/dosbox-SVN.conf:

[sblaster]
sbtype=none
oplmode=opl2
oplrate=49716
oplemu=opl2arduino
opl2arduino=/dev/ttyUSB0

Then, run DOSBox with ./src/dosbox. That's it!

You will likely get the "OPL2Arduino: too slow, consider increasing buffer" message a lot. To fix this, you need to recompile SerialIface.ino with a bigger receive buffer:

$ platformio ci \
    --board nanoatmega328 \
    --lib ../../src \
    --project-option="targets=upload" \
    --project-option="upload_port=/dev/ttyUSB0" \
    --project-option="build_flags=-DSERIAL_RX_BUFFER_SIZE=512" \
    SerialIface.ino

ScummVM🔗

The same code can be adapted for ScummVM (patch). To test, build it from source:

$ sudo apt build-dep scummvm
$ git clone https://github.com/vincentbernat/scummvm.git -b feature/opl2audioboard
$ cd scummvm
$ ./configure --disable-all-engines --enable-engine=scumm && make

Then, you can start ScummVM with ./scummvm. Select "AdLib Emulator" as the music device and "OPL2 Arduino" as the AdLib emulator.3 Like for DOSBox, watch the console to check if you need a larger receive buffer.

Enjoy! 😍

  1. This command is valid for an Arduino Nano. For another board, take a look at the output of platformio boards arduino. ↩︎

  2. Another World (also known as Out of This World), released in 1991, designed by Éric Chahi, is using sampled sounds at 5 kHz or 10 kHz. With a serial port operating at 115,200 bits/s, the 5 kHz option is just within our reach. However, I have no idea if the rendering is faithful. It doesn't sound like a SoundBlaster, but it sounds analogous to the rendering of the OPL2LPT which sounds similar to the SoundBlaster when using the 10 kHz option. DOSBox' AdLib emulation using Nuked OPL3-which is considered to be the best-sounds worse. ↩︎

  3. If you need to specify a serial port other than /dev/ttyUSB0, add a line opl2arduino_device= in the ~/.scummvmrc configuration file. ↩︎

21 Apr 2018 9:19am GMT

20 Apr 2018

feedPlanet Debian

Benjamin Mako Hill: Hyak on Hyak

I recently fulfilled a yearslong dream of launching a job on Hyak* on Hyak†.

Hyak on Hyak

* Hyak is the University of Washington's supercomputer which my research group uses for most of our computation-intensive research.
† M/V Hyak is a Super-class ferry operated by the Washington State Ferry System.

20 Apr 2018 10:26pm GMT

Jonathan Dowland: Twitter 10th anniversary

Tomorrow marks my 10th anniversary on Twitter. I have mixed feelings about the occasion. Twitter has been both a terrific success and a horrific failure. I've enjoyed it, I've discovered interesting people via Twitter and had some great interactions. I certainly prefer it to Facebook, but that's not a high benchmark.

Back in the early days I tried to engage with Twitter the way a hacker would. I worked out a scheme to archive my own tweets. I wrote a twitter bot. But Twitter became more and more hostile to that kind of interaction, so I no longer bother. Anything I put on Twitter I consider ephemeral. I've given up backing up my own tweets, conversations, or favourites. I deleted the bot. I keep a "sliding window" of recent tweets, outside of which I delete (via tweetdelete). My window started out a year wide; now it's down to three months.

Asides from the general hostility to third-parties wanting to build on the Twitter platform, they've also done a really poor job of managing bad actors. Of the the tools they do offer, they save the best for people with "verified" status: ostensibly a system for preventing fakes, now consider by some a status symbol. Twitter have done nothing to counter this, in fact they've actively encouraged it, by withdrawing it in at least one case from a notorious troll as an ad-hoc form of punishment. For the rest of us, the tools are woefully inadequate. If you find yourself on the receiving end of even a small pocket of bad attention, twitter becomes effectively unusable for hours or days on end. Finally troll-in-chief (and now President of the US) is inexplicably still permitted on Twitter despite repeatedly and egregiously violating their terms of service, demonstrating that there's different rules for some folks than the rest of us.

(By the way, I thoroughly recommend looking at Block Lists/Bots. I'm blocking thousands of accounts, although the system I've been using appears to have been abandoned. It might be worth a look at blocktogether.org; I intend to at some point.)

To some extent Twitter is responsible for-if not the death, the mortal wounding- of blogging. Back in the dim-and-distant, we'd write blog posts for the idle thoughts (e.g.), and they've migrated quite comfortably to tweets, but it seems to have had a sapping effect on people writing even longer-form stuff. Twitter isn't the only culprit: Google sunsetting Reader in 2013 was an even bigger blow, and I've still not managed to find something to replace it. (Plenty of alternatives exist; but the habit has died.)

One of the well-meaning, spontaneous things that came from the Twitter community was the notion of "Follow Friday": on Fridays, folks would nominate other interesting folks that you might like to follow. In that spirit, and wishing to try boost the idea of blogging again, I'd like to nominate some interesting blogs that you might enjoy. (Feel free to recommend me some more blogs to read in the comments!):

A couple of blogs from non-Debian/Linux OS developers. It's always nice to see what the other grass is like.

Finally, a more pleasing decennial: this year marks 10 years since my first uploaded package for Debian.

20 Apr 2018 1:25pm GMT