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. 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

I was playing around with parsing JSON in Scala, and got spray-json as recommendation from my Senpai. My aim was parsing some nested structure like:

  
  "key1" : "value1",
  "key2" :   "subkey1" : "subval1", "subkey2" : "subval2"  
 

into a nested Scala case class:

case class SubClass(subkey1: String, subkey2: String)
case class MainClass(key1: String, key2: SubClass)

To achieve this one needs to define one s own JsonProtocol that describes the parsing:

import spray.json._
object MyJsonProtocol extends DefaultJsonProtocol  
  implicit val subclassFormat = jsonFormat2(SubClass)
  implicit val mainclassFormat = jsonFormat2(MainClass)
 
import MyJsonProtocol._

Using this parsing can be done in the usual way:

val jsonstr = """
      
      "key1" : "value1",
      "key2" :   "subkey1" : "subval1", "subkey2" : "subval2"  
     
    """
val jsonAst = jsonstr.parseJson
val gotit = jsonAst.convertTo[MainClass]

If the input is from a JSON array of the above arrays:

[
    
    "key1" : "value1",
    "key2" :   "subkey1" : "subval1", "subkey2" : "subval2"  
   ,
    
    "key1" : "value10",
    "key2" :   "subkey1" : "subval10", "subkey2" : "subval20"  
   
]

the only change necessary is to call

val gotit = jsonAst.convertTo[List[MainClass]]

For quite some time I have some cryptocurrencies on hold. These mostly come from times it was possible to mine Bitcoin on the CPU, but I've got some small payments recently as well. I've been using Electrum wallet so far. It worked quite well, but with increasing Bitcoin value, I was considering having some hardware wallet for that. There are few options which you can use, but I've always preferred Trezor as that device is made by guys I know. Also it's probably device with best support out of these (at least I've heard really bad stories about Ledger support). In the end what decided is that they are also using Weblate to translate their user interface and offered me the wallet for free in exchange. This is price you can not beat :-). Anyway the setup was really smooth and I'm now fully set up. This also made me more open to accept other cryptocurrencies which are supported by Trezor, so you can now see more options on the Weblate donations page.

Filed under: Debian English SUSE Weblate

Three years ago I referenced the Seinfeld Streak used in an earlier post of regular updates to to the Rcpp Gallery:

This is sometimes called Jerry Seinfeld's secret to productivity: Just keep at it. Don't break the streak.

and showed the first chart of GitHub streaking

And two year ago a first follow-up appeared in this post:

And a year ago we had a followup last year

And as it October 12 again, here is the new one:

Again, special thanks go to Alessandro Pezz for the Chrome add-on GithubOriginalStreak.

This post by Dirk Eddelbuettel originated on his Thinking inside the box blog. Please report excessive re-aggregation in third-party for-profit settings.

Often, when I mention how things work in the interactive theorem prover [Isabelle/HOL] (in the following just Isabelle ¹) 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 it². 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?³ 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 perform⁴, 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.

We are thrilled to announce a new big RcppArmadillo release! Conrad recently moved Armadillo to the 8.* series, with significant improvements and speed ups for sparse matrix operations, and more. See below for a brief summary. This also required some changes at our end which Binxiang Ni provided, and Serguei Sokol improved some instantiations. We now show the new vignette Binxiang Ni wrote for his GSoC contribution, and I converted it (and the other main vignette) to using the pinp package for sleeker pdf vignettes. This release resumes our bi-monthly CRAN release cycle. I may make interim updates available at GitHub "as needed". And this time I managed to mess up the reverse depends testing, and missed one sync() call on the way back to R---but all that is now taken care of. Armadillo is a powerful and expressive C++ template library for linear algebra aiming towards a good balance between speed and ease of use with a syntax deliberately close to a Matlab. RcppArmadillo integrates this library with the R environment and language--and is widely used by (currently) 405 other packages on CRAN. A high-level summary of changes follows.

Changes in RcppArmadillo version 0.8.100.1.0 (2017-10-05)

• Upgraded to Armadillo release 8.100.1 (Feral Pursuits)
  • faster incremental construction of sparse matrices via element access operators
  • faster diagonal views in sparse matrices
  • expanded SpMat to save/load sparse matrices in coord format
  • expanded .save(),.load() to allow specification of datasets within HDF5 files
  • added affmul() to simplify application of affine transformations
  • warnings and errors are now printed by default to the std::cerr stream
  • added set_cerr_stream() and get_cerr_stream() to replace set_stream_err1(), set_stream_err2(), get_stream_err1(), get_stream_err2()
  • new configuration options ARMA_COUT_STREAM and ARMA_CERR_STREAM
• Constructors for sparse matrices of types dgt, dtt amd dst now use Armadillo code for improved performance (Serguei Sokol in #175 addressing #173)
• Sparse matrices call .sync() before accessing internal arrays (Binxiang Ni in #171)
• The sparse matrix vignette has been converted to Rmarkdown using the pinp package, and is now correctly indexed. (#176)

Courtesy of CRANberries, there is a diffstat report. More detailed information is on the RcppArmadillo page. Questions, comments etc should go to the rcpp-devel mailing list off the R-Forge page.

This post by Dirk Eddelbuettel originated on his Thinking inside the box blog. Please report excessive re-aggregation in third-party for-profit settings.

It feels like the past week or two has been very busy, and so I'm looking forward to my "holiday" next month. I'm not really having a holiday of course, my wife is slowly returning to work, so I'll be taking a month of paternity leave, taking sole care of Oiva for the month of November. He's still a little angel, and now that he's reached 10 months old he's starting to get much more mobile - he's on the verge of walking, but not quite there yet. Mostly that means he wants you to hold his hands so that he can stand up, swaying back and forth before the inevitable collapse. Beyond spending most of my evenings taking care of him, from the moment I return from work to his bedtime (around 7:30PM), I've made the Debian Administration website both read-only and much simpler. In the past that site was powered by a lot of servers, I think around 11. Now it has only a small number of machines, which should slowly decrease. I've ripped out the database host, the redis host, the events-server, the planet-machine, the email-box, etc. Now we have a much simpler setup:

• Front-end machine
  • Directly serves the code site
  • Directly serves the SSL site which exists solely for Let's Encrypt
  • Runs HAProxy to route the rest of the requests to the cluster.
• 4 x Apache servers
  • Each one has a (read-only) MySQL database on it for the content.
    • In case of future-compromise I removed all user passwords, and scrambled the email-addresses.
    • I don't think there's a huge risk, but better safe than sorry.
  • Each one runs the web-application.
    • Which now caches each generated page to /tmp/x/x/x/x/$hash if it doesn't exist.
    • If the request is cached it is served from that cache rather than dynamically.

Finally although I'm slowly making progress with "radio stuff" I've knocked up a simple hack which uses an ultrasonic sensor to determine whether I'm sat in front of my (home) PC. If I am everything is good. If I'm absent the music is stopped and the screen locked. Kinda neat. (Simple ESP8266 device wired to the sensor. When the state changes a message is posted to Mosquitto, where a listener reacts to the change(s).) Oh, not final. I've also transfered my mobile phone from DNA.fi to MoiMobile. Which should complete soon, right now my phone is in limbo, active on niether service. Oops.

Hosted Weblate provides also free hosting for free software projects. The hosting requests queue has grown too long, so it's time to process it and include new project. This time, the newly hosted projects include:

• Hunspell - famous spell checker
• Eolie - a web browser for GNOME
• SkyTube - an open-source YouTube app for Android
• Eventum - issue tracking system

Additionally there were some notable additions to existing projects:

• Password management module for Pext
• Minetest Mod Hopper
• Ayatana Indicators now include several new applets

If you want to support this effort, please donate to Weblate, especially recurring donations are welcome to make this service alive. You can do that easily on Liberapay or Bountysource.

Filed under: Debian English SUSE Weblate

During a long era, electronic mail was the main communication tool for enterprises. Slack, which offer public or private group discussion boards and instant messaging between two people, challenge its position, especially in the IT industry. Not only Slack has features known and used since IRC launch in the late 80s, but Slack also offers file sending and sharing, code quoting, and it indexing for ulterior searches everything that goes through the application. Slack is also modular with numerous plug-in to easily add new features. Using the Software-As-A-Service (SAAS) model, Slack basic version is free, and users pay for options. Slack is now considered by the Github generation like the new main enterprise communication tool. As I did in my previous article on the Github threat, this one won t promote Slask s advantages, as many other articles have already covered all these points ad nauseam, but to show the other side and to warn the companies using this service about its inherent risks. So far, these risks have been ignored, sometimes voluntary in the name of the It works ideology. Neglecting all economic and safety consideration, neglecting all threat to privacy and individual freedom. We ll see about them below. All your company communication since its creation When a start-up chooses Slack, all of its internal communication will be stored by Slack. When someone uses this service, the simple fact to chat through it means that the whole communication is archived. One may point that within the basic Slack offer, only the last 10.000 messages can be read and searched. Bad argument. Slack stored every message and every file shared as it pleases. We ll see below this application behavior is of capital importance in the Slack threat to enterprises. And the problem is the same for all other companies which choose Slack at one point or another. If they replace their traditional communication method with it, Slack will have access to capital data, not only in volume, but also because of their value for the company itself Or anyone interested in this company life. Search Your Entire Archive One of the main arguments to use Slack is its Search your entire archive feature. One can search almost anything one can think of. Why? Because everything is indexed. Your team chat archive or the more or less confidential documents exchanged with the accountant department; everything is in it in order to provide the most effective search tool. We can t deny it s a very attractive feature for everyone inside the company. But it is also a very attractive feature for everyone outside of the company who would want to know more about its internal life. Even more if you re looking for a specific subject. If Slack is the main communication tool of your company, and if as I ve experienced in my professional life, some teams prefer to use it than to go to the office next door or even bug you to put the information on the dedicated channel, one can easily deduce that nothing in this type of company escape Slack. The automatic indexation and the search feature efficiency are excellent tools to get all the information needed, in quantity and in quality. As such, it s a great social engineering tool for everyone who has access to it, with a history as old as the use of Slack as a communication tool in the company. Across borders And Beyond! Slack is a Web service which uses mainly Amazon Web services and most specially Cloudfront, as stated by the available information on Slack infrastructure. Even without a complete study of said infrastructure, it s easy to state that all the data regarding many innovative global companies around the world (and some of them including for all their internal communication since their creation) are located in the United States, or at least in the hands of a US company, which must follow US laws, a country with a well-known history of large scale industrial espionage, as the whistleblower Edward Snowden demonstrated it in 2013 and where company data access has no restriction under the Patriot Act, as in the Microsoft case (2014) where data stored in Ireland by the Redmond software editor have been given to US authorities. As such, Slack s automatic indexation and search tool are a boon for anyone spy agency or hacker which get authorized access to it. To trust a third party with all, or at least most of, your internal corporate communication is a certain risk for your company if the said third party doesn t follow the same regulations as yours or if it has different interests, from a data security point of view or more globally on its competitiveness. A badly timed data leak can be catastrophic. What s the point of secretly preparing a new product launch or an aggressive takeover if all your recent Slack conversations have leaked, including your secret plans? What if Slack is hacked? First let s remember that even if a cyber attack may appear as a rare or hypothetical scenario to a badly informed and hurried manager, it is far from being as rare as she or he believes it (or wants to believe it). Infrastructure hacking is quite common, as a regular visit to Hacker News will give you multiple evidence. And Slack itself has already been hacked. February 2015: Slack is the victim during four days of a cyber attack, which was made public by the company in March. Officially, the unauthorized access was limited to information on the users profiles. It is impossible to measure exactly what and who was impacted by this attack. In a recent announcement, Yahoo confessed that these 3 billion accounts (you ve read well: 3 billions) were compromised late 2014! Officially, Slack stated that No financial or payment information was accessed or compromised in this attack. Which is, and by far, the least interesting of all data stored within Slack! With company internal communication indexed sometimes from the very beginning of said company and searchable, Slack may be a potential target for cybercriminal not looking for its users financial credentials but more their internal data already in a usable format. One can imagine Slack must give information on a massive data leak, which can t be ignored. But what would happen if only one Slack user is the victim of said leak? The Free Alternative Solutions As we demonstrated above, companies need to find an alternative solution to Slack, one they can host themselves to reduce data leaks and industrial espionage and dependency on the Internet connection. Luckily, Slack success created its own copycats, some of them being also free software. Rocket.chat is one of them. Its comprehensive service offers chat rooms, direct messages and file sharing but also videoconferencing and screen sharing, and even most features. Check their dedicated page. You can also try an online demo. And even more, Rocket Chat has a very simple extension system and an API. Mattermost is another service which has the advantages of proximity and of compatibility with Slack. It offers numerous features including the main expected by this type of software. It also offers numerous apps and plug-ins to interact with online services, software forges, and continuous integration tools. It works In the introduction, we discussed the It works effect, usually invoked to dispel any arguments about data protection and exchange confidentiality we discussed in this article. True, one single developer can ask: why worry about it? All I want is to chat with my colleagues and send files! Because Slack service subscription in the long term put the company continuously at risk. Maybe it s not the employees place to worry about it, they just have to do their job the more efficiently possible. On the other side, the company management, usually non-technical, may not be aware of what risks will threaten their company with this technical choice. The technical management may pretend to be omniscient, nobody is fooled. Either someone from the direction will ask the right question (where are our data and who can access them?) or someone from the technical side alert them officially on these problems. This is this technical audience, even if not always heard by their direction, which is the target of this article. May they find in it the right arguments to be convincing. We hope that the several points we developed in this article will help you to make the right choice. About Me Carl Chenet, Free Software Indie Hacker, founder of the French-speaking Hacker News-like Journal du hacker. Follow me on social networks

• My Mastodon account : @carlchenet
• My Diaspora* account : @carlchenet
• My Twitter account : @carl_chenet

Translated from French by St phanie Chaptal. Original article written in October 2016.

A long time ago, I switched my GnuPG setup to a smartcard based one. I kept using the same master key, but:

• copied the rsa4096 master key to a master smartcard, for when I need to sign (certify) other keys;
• created rsa2048 subkeys (for signature, encryption and authentication) and moved them to an OpenPGP smartcard for daily usage.

I've been working with that setup for a few years now and it is working perfectly fine. The signature counter on the OpenPGP basic card is a bit north of 5000 which is large but not that huge, all considered (and not counting authentication and decryption key usage).

One very nice feature of using a smartcard is that my laptop (or other machines I work on) never manipulates the private key directly but only sends request to the card, which is a really huge improvement, in my opinion. But it's also not the perfect solution for me: the OpenPGP card uses a proprietary platform from ZeitControl, named BasicCard. We have very few information on the smartcard, besides the fact that Werner Koch trust ZeistControl to not mess up. One caveat for me is that the card does not use a certified secure microcontroler like you would find in smartcard chips found in debit card or electronic IDs. That means it's not really been audited by a competent hardware lab, and thus can't be considered secure against physical attacks. The cardOS software and the application implementing the OpenPGP specification are not public either and have not been audited either, to the best of my knowledge.

At one point I was interested in the Yubikey Neo, especially since the architecture Yubico used was common: a (supposedly) certified platform (secure microcontroler, card OS) and a GlobalPlatform / JavaCard virtual machine. The applet used in the Yubikey Neo is open-source, too, so you could take a look at it and identify any issue.

Unfortunately, Yubico transitioned to a less common and more proprietary infrastructure for Yubikey 4: it's not longer Javacard based, and they don't provide the applet source anymore. This was not really seen as a good move by a lot of people, including Konstantin Ryabitsev (kernel.org administrator). Also, it wasn't possible even for the Yubico Neo to actually build the applet yourself and inject it on the card: when the Yubikey leaves the facility, the applet is already installed and the smartcard is locked (for obvious security reason). I've tried asking about getting naked/empty Yubikey with developers keys to load the applet myself, but it' was apparently not possible or would have required signing an NDA with NXP (the chip maker), which is not really possible as an individual (not that I really want to anyway).

In the meantime, a coworker actually wrote an OpenPGP javacard applet, with the intention to support latest version of the OpenPGP specification, and especially elliptic curve cryptography. The applet is called SmartPGP and has been released on ANSSI github repository. I investigated a bit, and found a smartcard with correct specification: certified (in France or Germany), and supporting Javacard 3.0.4 (required for ECC). The card can do RSA2048 (unfortunately not RSA4096) and EC with NIST (secp256r1, secp384r1, secp521r1) and Brainpool (P256, P384, P512) curves.

I've ordered some cards, and when they arrived started playing. I've built the SmartPGP applet and pushed it to a smartcard, then generated some keys and tried with GnuPG. I'm right now in the process of migrating to a new smartcard based on that setup, which seems to work just fine after few days.

Part two of this serie will describe how to build the applet and inject it in the smartcard. The process is already documented here and there, but there are few things not to forget, like how to lock the card after provisionning, so I guess having the complete process somewhere might be useful in case some people want to reproduce it.

Upcoming Weblate 2.17 will bring improved access control settings. Previously this could be controlled only by server admins, but now the project visibility and access presets can be configured. This allows you to better tweak access control for your needs. There is additional choice of making the project public, but restricting translations, what has been requested by several projects. You can see the possible choices on the UI screenshot: On Hosted Weblate this feature is currently available only to commercial hosting customers. Projects hosted for free are limited to public visibility only.

Filed under: Debian English SUSE Weblate

The @TorAtlas web application will now also prompt operators to update their relays if they are outdated. pic.twitter.com/HMixwqbBKM Tor Atlas (@TorAtlas) October 9, 2017

We have instructions for setting up new Tor relays on Debian. The only time the word upgrade is mentioned here is:

Be sure to set your ContactInfo line so we can contact you if you need to upgrade or something goes wrong.

This isn t great. We should have some decent instructions for keeping your relay up to date too. I ve been compiling a set of documentation for enabling automatic updates on various Linux distributions, here s a taste of what I have so far:

---

Debian Make sure that unattended-upgrades is installed and then enable the installation of updates (as root):

apt install unattended-upgrades
dpkg-reconfigure -plow unattended-upgrades

Fedora 22 or later Beginning with Fedora 22, you can enable automatic updates via:

dnf install dnf-automatic

In /etc/dnf/automatic.conf set:

apply_updates = yes

Now enable and start automatic updates via:

systemctl enable dnf-automatic.timer
systemctl start dnf-automatic.timer

(Thanks to Enrico Zini I know all about these timer units in systemd now.)

RHEL or CentOS For CentOS, RHEL, and older versions of Fedora, the yum-cron package is the preferred approach:

yum install yum-cron

In /etc/yum/yum-cron.conf set:

apply_updates = yes

Enable and start automatic updates via:

systemctl start yum-cron.service

---

I d like to collect together instructions also for other distributions (and *BSD and Mac OS). Atlas knows which platform a relay is running on, so there could be a link in the future to some platform specific instructions on how to keep your relay up to date.

It's not easy getting Docker to work in Debian. It's not in stable at all:

0 jamie@turkey:~$ rmadison docker.io
docker.io    1.6.2~dfsg1-1~bpo8+1   jessie-backports   source, amd64, armel, armhf, i386
docker.io    1.11.2~ds1-5           unstable           source, arm64
docker.io    1.11.2~ds1-5           unstable-debug     source
docker.io    1.11.2~ds1-6           unstable           source, armel, armhf, i386, ppc64el
docker.io    1.11.2~ds1-6           unstable-debug     source
docker.io    1.13.1~ds1-2           unstable           source, amd64
docker.io    1.13.1~ds1-2           unstable-debug     source
0 jamie@turkey:~$ 

And a problem with runc makes it really hard to get it working on Debian unstable. These are the steps I took to get it running today (2017-10-10). Remove runc (allow it to remove containerd and docker.io):

sudo apt-get remove runc

Install docker-runc (now in testing)

sudo apt-get install docker-runc

Fix containerd package to depend on docker-runc instead of runc:

mkdir containerd
cd containerd
apt-get download containerd 
ar x containerd_0.2.3+git20170126.85.aa8187d~ds1-2_amd64.deb
tar -xzf control.tar.gz
sed -i s/runc/docker-runc/g control
tar -c md5sums control   gzip -c > control.tar.gz
ar rcs new-containerd.deb debian-binary control.tar.gz data.tar.xz
sudo dpkg -i new-containerd.deb

Fix docker.io package to depend on docker-runc instead of runc.

mkdir docker
cd docker
apt-get download docker.io
ar x docker.io_1.13.1~ds1-2_amd64.deb
tar -xzf control.tar.gz
sed -i s/runc/docker-runc/g control
tar -c  post,pre inst,rm  md5sums control   gzip -c > control.tar.gz
ar rcs new-docker.io.deb debian-binary control.tar.gz data.tar.xz
sudo dpkg -i new-docker.io.deb

Symlink docker-runc => runc

sudo ln -s /usr/sbin/docker-runc /usr/sbin/runc

Keep apt-get from upgrading until this bug is fixed:

printf "# Remove when docker.io and containerd depend on docker-runc
# instead of normal runc
# https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=877329
Package: runc 
Pin: release * 
Pin-Priority: -1 
Package: containderd 
Pin: release * 
Pin-Priority: -1 
Package: docker.io
Pin: release * 
Pin-Priority: -1"   sudo tee /etc/apt/preferences.d/docker.pref

Thanks to coderwall for tips on manipulating deb files.

Here's what happened in the Reproducible Builds effort between Sunday October 1 and Saturday October 7 2017: Media coverage

• Bernhard sent another report about the status of Reproducible openSUSE. They currently they are at 478 unreproducible and 11,111 reproducible packages out of 11,821, so also at 93%!
• Holger attempted to get a Reproducible Builds devroom at FOSDEM 2018 but sadly this proposal was not accepted.

Documentation updates

• Christoph Berg created a wiki page about Openjade generated timestamps from DSSSL stylesheets.

Packages reviewed and fixed, and bugs filed

• Bernhard M. Wiedemann:
  • LiE uninitialized memory (need to find upstream)
  • chrony date (merged)
• Chris Lamb:
  • #877375 filed against polygen.
  • #877381 filed against plr.
  • #877384 filed against rcs.
  • #877928 filed against cadvisor.
• jathan:
  • #877470 filed against bsh.

Reviews of unreproducible packages 32 package reviews have been added, 46 have been updated and 62 have been removed in this week, adding to our knowledge about identified issues. Weekly QA work During our reproducibility testing, FTBFS bugs have been detected and reported by:

• Adrian Bunk (27)

diffoscope development

• Chris Lamb:
  • Don't crash on malformed md5sums files. (Closes: #877473)
  • Improve names in output of "internal" binwalk members. (Closes: #877525)
• Mattia Rizzolo:
  • Fix test compatibility with dtb version 1.4.5

strip-nondeterminism development Rob Browning noticed that strip-nondeterminism was causing serious performance regressions in the Clojure programming language within Debian. After some discussion, Chris Lamb also posted a query to debian-devel in case there were any other programming languages that might be suffering from the same problem.

• Chris Lamb:
  • jar.pm: Clojure considers the .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.. (Closes: #877418)
  • jar.pm, zip.pm: Allow $options member_normalizer callback to support specifying the timestamp.
  • zip.pm: Ensure that we don't try and write an old timestamp; Archive::Zip will do this anyway, just noisily.
  • zip.pm: Calculate the target canonical time in just one place.
  • bin/strip-nondeterminism: Print a warning in --verbose mode if no canonical time specified.
  • jar.pm: Update comment to reflect that NTFS/FAT has a 2s timestamp granularity.
  • jar.pm: s/NTFS/FAT/. Thanks to James Ross.

reprotest development Versions 0.7.1 and 0.7.2 were uploaded to unstable by Ximin Luo:

• New features:
  • Add a --auto-build option to try to determine which specific variations cause unreproducibility.
  • Add a --source-pattern option to restrict copying of source_root, and set this automatically in our presets.
• Usability improvements:
  • Improve error messages in some common scenarios.
    • Fiving a source_root or build_command that doesn't exist
    • Using reprotest with default settings after not installing Recommends
  • Output hashes after a successful --auto-build.
  • Print a warning message if we reproduced successfully but didn't vary everything.
• Fix varying both umask and user_group at the same time.
• Have dpkg-source extract to different build dir if varying the build-path.
• Pass --exclude-directory-metadata to diffoscope(1) by default as this is the majority use-case.
• Various bug fixes to get the basic dsc+schroot example working.

It included contributions already covered by posts of the previous weeks, as well as new ones from:

• Ximin Luo:
  • main: Add a --env-build option for testing different env vars
  • Don't output spurious warnings in tests
  • Add some more notes on the remaining variations
  • Fix the help text for virtual servers

tests.reproducible-builds.org

• Mattia Rizzolo:
  • Re-deploy odxu4a after being reinstalled and renamed from odxu4.
• Vagrant Cascadian:
  • Rename armhf host odxu4 to odxu4a

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

QSoas can read and execute Ruby code directly, while reading command files, or even at the command prompt. For that, just write plain Ruby code inside a ruby...ruby end block. Probably the most useful possibility is to define elaborated functions directly from within QSoas, or, preferable, from within a script; this is an alternative to defining a function in a completely separated Ruby-only file using ruby-run. For instance, you can define a function for plain Michaelis-Menten kinetics with a file containing:

ruby
def my_func(x, vm, km)
  return vm/(1 + km/x)
end
ruby end

This defines the function my_func with three parameters, , (vm) and (km), with the formula:

You can then test that the function has been correctly defined running for instance:

QSoas> eval my_func(1.0,1.0,1.0)
 => 0.5
QSoas> eval my_func(1e4,1.0,1.0)
 => 0.999900009999

This yields the correct answer: the first command evaluates the function with x = 1.0, vm = 1.0 and km = 1.0. For , the result is (here 0.5). For , the result is almost . You can use the newly defined my_func in any place you would use any ruby code, such as in the optional argument to generate-buffer, or for arbitrary fits:

QSoas> generate-buffer 0 10 my_func(x,3.0,0.6)
QSoas> fit-arb my_func(x,vm,km)

To redefine my_func, just run the ruby code again with a new definition, such as:

ruby
def my_func(x, vm, km)
  return vm/(1 + km/x**2)
end
ruby end

The previous version is just erased, and all new uses of my_func will refer to your new definition.


See for yourselfThe code for this example can be found there. Browse the qsoas-goodies github repository for more goodies !

About QSoasQSoas is a powerful open source data analysis program that focuses on flexibility and powerful fitting capacities. It is released under the GNU General Public License. It is described in Fourmond, Anal. Chem., 2016, 88 (10), pp 5050 5052. Current version is 2.1. You can download its source code or buy precompiled versions for MacOS and Windows there.

Welcome to gambaru.de. Here is my monthly report that covers what I have been doing for Debian. If you re interested in Java, Games and LTS topics, this might be interesting for you. Debian Games

• I sponsored a new release of hexalate for Unit193 and icebreaker for Andreas Gnau. The latter is a reintroduction.
• New upstream releases this month: freeorion and hyperrogue.
• I backported freeciv and freeorion to Stretch.

Debian Java

• New upstream releases and one update: sweethome3d, sweethome3d-furniture, sweethome3d-furniture-editor, sweethome3d-textures-editor (update), libsambox-java, libsejda-java, pdfsam, easymock, jboss-modules, jboss-xnio and undertow.
• I fixed one RC bug in libsejda-io-java (#874494) and investigated another one (#869266) in commons-httpclient which could be closed.
• The new build-dependencies of jboss-xnio, wildfly-client-config and wildfly-common, were accepted into the archive this month.
• I spent some quality time on fixing #874579 in libhibernate-validator-java. This was the last blocking bug for pdfsam which I could finally upload to unstable. It s a really great JavaFX application. Check it out!
• I sponsored another update of libimglib2-java for Ghislain Vaillant and simplyhtml, freeplane and knopflerfish-osgi for Felix Natter.
• I also fixed RC bug #871348 in robocode, a Java programming game and #871347 in tycho.

Debian LTS This was my nineteenth month as a paid contributor and I have been paid to work 15,75 hours on Debian LTS, a project started by Rapha l Hertzog. In that time I did the following:

• From 18. September to 24. September I was in charge of our LTS frontdesk. I triaged bugs in poppler, binutils, kannel, wordpress, libsndfile, libexif, nautilus, libstruts1.2-java, nvidia-graphics-drivers, p3scan, otrs2 and glassfish.
• DLA-1108-1. Issued a security update for tomcat7 fixing 1 CVE.
• DLA-1116-1. Issued a security update for poppler fixing 3 CVE.
• DLA-1119-1. Issued a security update for otrs2 fixing 4 CVE.
• DLA-1122-1. Issued a security update for asterisk fixing 1 CVE. I also investigated CVE-2017-14099 and CVE-2017-14603. I decided against a backport because the fix was too intrusive and the vulnerable option is disabled by default in Wheezy s version which makes it a minor issue for most users.
• I submitted a patch for Debian s reportbug tool. (#878088) During our LTS BoF at DebConf 17 we came to the conclusion that we should implement a feature in reportbug that checks whether the bug reporter wants to report a regression for a recent security update. Usually the LTS and security teams receive word from the maintainer or users who report issues directly to our mailing lists or IRC channels. However in some cases we were not informed about possible regressions and the new feature in reportbug shall ensure that we can respond faster to such reports.
• I started to investigate the open security issues in wordpress and will complete the work in October.

Misc

• I packaged a new version of xarchiver. Thanks to the work of Ingo Br ckl xarchiver can handle almost all archive formats in Debian now.

QA upload

• I did a QA upload of xball, an ancient game from the 90ies that simulates bouncing balls. It should be ready for another decade at least.

Thanks for reading and see you next time.

I was assigned 15 hours of work by Freexian's Debian LTS initiative and carried over 6 hours from August. I only worked 12 hours, so I will carry over 9 hours to the next month. I prepared and released another update on the Linux 3.2 longterm stable branch (3.2.93). I then rebased the Debian linux package onto this version, added further security fixes, and uploaded it (DLA-1099-1).

Upcoming Weblate 2.17 will bring improved access control settings. Previously this could be controlled only by server admins, but now the project visibility and access presets can be configured. This allows you to better tweak access control for your needs. There is additional choice of making the project public, but restricting translations, what has been requested by several projects. You can see the possible choices on the UI screenshot: On Hosted Weblate this feature is currently available only to commercial hosting customers. Projects hosted for free are limited to public visibility only.

Filed under: Debian English SUSE Weblate

Introduction pristine-tar is a tool that is present in the workflow of a lot of Debian people. I adopted it last year after it has been orphaned by its creator Joey Hess. A little after that Tomasz Buchert joined me and we are now a functional two-person team. pristine-tar goals are to import the content of a pristine upstream tarball into a VCS repository, and being able to later reconstruct that exact same tarball, bit by bit, based on the contents in the VCS, so we don t have to store a full copy of that tarball. This is done by storing a binary delta files which can be used to reconstruct the original tarball from a tarball produced with the contents of the VCS. Ultimately, we want to make sure that the tarball that is uploaded to Debian is exactly the same as the one that has been downloaded from upstream, without having to keep a full copy of it around if all of its contents is already extracted in the VCS anyway. The current state of the art, and perspectives for the future pristine-tar solves a wicked problem, because our ability to reconstruct the original tarball is affected by changes in the behavior of tar and of all of the compression tools (gzip, bzip2, xz) and by what exact options were used when creating the original tarballs. Because of this, pristine-tar currently has a few embedded copies of old versions of compressors to be able to reconstruct tarballs produced by them, and also rely on a ever-evolving patch to tar that is been carried in Debian for a while. So basically keeping pristine-tar working is a game of Whac-A-Mole. Joey provided a good summary of the situation when he orphaned pristine-tar. Going forward, we may need to rely on other ways of ensuring integrity of upstream source code. That could take the form of signed git tags, signed uncompressed tarballs (so that the compression doesn t matter), or maybe even a different system for storing actual tarballs. Debian bug #871806 contains an interesting discussion on this topic. Recent improvements Even if keeping pristine-tar useful in the long term will be hard, too much of Debian work currently relies on it, so we can t just abandon it. Instead, we keep figuring out ways to improve. And I have good news: pristine-tar has recently received updates that improve the situation quite a bit. In order to be able to understand how better we are getting at it, I created a "visualization of the regression test suite results. With the help of data from there, let s look at the improvements made since pristine-tar 1.38, which was the version included in stretch. pristine-tar 1.39: xdelta3 by default. This was the first release made after the stretch release, and made xdelta3 the default delta generator for newly-imported tarballs. Existing tarballs with deltas produced by xdelta are still supported, this only affects new imports. The support for having multiple delta generator was written by Tomasz, and was already there since 1.35, but we decided to only flip the switch after using xdelta3 was supported in a stable release. pristine-tar 1.40: improved compression heuristics pristine-tar uses a few heuristics to produce the smaller delta possible, and this includes trying different compression options. In the release Tomasz included a contribution by Lennart Sorensen to also try the --gnu, which gretly improved the support for rsyncable gzip compressed files. We can see an example of the type of improvement we got in the regression test suite data for delta sizes for faad2_2.6.1.orig.tar.gz: pristine-tar 1.41: support for signatures This release saw the addition of support for storage and retrieval of upstream signatures, contributed by Chris Lamb. pristine-tar 1.42: optionally recompressing tarballs I had this idea and wanted to try it out: most of our problems reproducing tarballs come from tarballs produced with old compressors, or from changes in compressor behavior, or from uncommon compression options being used. What if we could just recompress the tarballs before importing then? Yes, this kind of breaks the pristine bit of the whole business, but on the other hand, 1) the contents of the tarball are not affected, and 2) even if the initial tarball is not bit by bit the same that upstream release, at least future uploads of that same upstream version with Debian revisions can be regenerated just fine. In some cases, as the case for the test tarball util-linux_2.30.1.orig.tar.xz, recompressing is what makes it possible to reproduce the tarball (and thus import it with pristine-tar) possible at all: In other cases, if the current heuristics can t produce a reasonably small delta, recompressing makes a huge difference. It s the case for mumble_1.1.8.orig.tar.gz: Recompressing is not enabled by default, and can be enabled by passing the --recompress option. If you are using pristine-tar via a wrapper tool like gbp-buildpackage, you can use the $PRISTINE_TAR environment variable to set options that will affect any pristine-tar invocations. Also, even if you enable recompression, pristine-tar will only try it if the delta generations fails completely, of if the delta produced from the original tarball is too large. You can control what too large means by using the --recompress-threshold-bytes and --recompress-threshold-percent options. See the pristine-tar(1) manual page for details.

Stardicter 1.1, the set of scripts to convert some freely available dictionaries to StarDict format, has been released today. The biggest change is that it will also keep source data together with generated dictionaries. This is good for licensing reasons and will also allow to actually build these as packages within Debian. Full list of changes:

• Various cleanups for first stable release.
• Fixed generating of README for dictionaries.
• Added support for generating source tarballs.
• Fixed installation on systems with non utf-8 locale.

As usual, you can install from pip, download source or download generated dictionaries from my website. The package should be soon available in Debian as well.

Filed under: Debian English StarDict