How to setup Rocq on Windows

Using the rocq platform binary installer for Windows:

 https://rocq-prover.org/install#windows-vscode

To let rocq know the binary and library directories

 - $env:COQBIN = "C:\rocq\bin"

 - $env:ROCQLIB = "C:\rocq\lib\coq"

To run rocq everywhere

 - $env:PATH += ";C:\rocq\bin"

I do not understand why this information is not available on the web site of Rocq!

How to build and run the Rust implementation of tree-sitter

 How to build the Rust implementation of tree-sitter

$ sudo ./script/build-wasm

  (Note just running the script might go wrong due to the permission error when it attempts to access the docker.)

$ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

  (This installs rustc, the latest rust compiler at ~/.cargo as guided in https://rustup.rs/.)

$ source ~/.cargo/env

 (This activates the path of the installed rust toolchains.)

$ cargo build

 (This builds tree-sitter with the installed rust toolchains. With no option to the build mode, tree-sitter is built in a debug mode that provides various debug options. Alternatively, one can give --release to the build mode for a release.)

How to run tree-sitter, say, over tree-sitter-python?

$ curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.40.1/install.sh | bash

  (Note one needs to setup nvm to install npm and other javascript relevant tools.)

$ nvm  install --lts

  (Install the latest npm and others.)

$ git clone https://github.com/tree-sitter/tree-sitter-python

  (For example, let us consider tree-sitter-python, which is a python parser using tree-sitter and uses an external its own lexer implementation not using tree-sitter.)

$ cd tree-sitter-python

Define TREE_SITTER as a release binary or a debug binary. 

• export TREE_SITTER=/home/khchoi/work/lang/tree-sitter/tree-sitter/target/debug/tree-sitter
• export TREE_SITTER=/home/khchoi/work/lang/tree-sitter/tree-sitter/target/release/tree-sitter

$ $TREE-SITTER generate --debug-build

 (Assuming $TREE-SITTER is a path to the tree-sitter directory, it generates src/parser.c and others. At this moment, it is unclear to me what is the effect of giving --debug-build to the generate mode.)

$ $TREE-SITTER build --debug

 (It changes ./src/node-types.json.)

$ $TREE-SITTER parse --debug YOUR-PYTHON-PROGRAM.py

 (It prints various logs including parsing actions and states, and then it prints an abstract syntax tree for the python program.)

Fixing an error "commitAndReleaseBuffer: invalid argument (invalid character)" in stack-building Haskell

 

On Windows, I often meet this annoying error:

 - stack build

   ...

   commitAndReleaseBuffer: invalid argument (invalid character)

   ...

This error seems to happen due to a locale setting on Windows. To see what is set for the locale, you can try the following PowerShell commands: 

 - Get-WinSystemLocale

 - Set-WinSystemLocale en-US

My locale was set for Korean. I changed it to en-US, and the error was magically gone away!

The locale setting command should run on PowerShell under the system manager mode.

On Ubuntu, I have rarely seen such an error, "commitAndReleaseBuffer: invalid argument (invalid character)".

More important thing: such an error is not just solely from locale settings, but it is actually caused by some real error in the haskell program to build. 

My guess is that there is something wrong in a Haskell program. Haskell stack or ghc detects it. It tries to write something about the detected error somewhere (perhaps, using SQL?), and the relevant Haskell library meets a locale setting problem, producing this famous error message:

  - commitAndReleaseBuffer: invalid argument (invalid character)

Fixing a space leak in a Haskell program: an experience report.

Wow! It is exciting to find and fix a space leak in my Haskell program, YAPB

 - https://github.com/kwanghoon/yapb : Commit #57c03df

1. Background

As a background, YAPB is a programmable parser building system based on LALR(1). I have been working on this for a few years. You can directly write parser specifications  in Haskell, not in Happy, Yacc, MLYacc, and so on. 

Using this tool, I have developed several parsers: PolyRPC, Small Basic, and C11. 

 - PolyRPC: an experimental (multi-tier) functional programming language (94 production rules)

 - Small Basic: Microsoft Small Basic (60 production rules)

 - C11: C11 standard (334 production rules)

For the three parser specifications, YAPB has successfully produced LALR(1) automations. 

(Note: I have also experiment this tool with Haskell (815 production rules) but in this case, I did not write a parser specification but I used the automation generated by Happy.)

2. A Space Leak Problem and a Solution

For PolyRPC and Small Basic parser specifications, YAPB shows no problem at all in terms of memory usages, though it does not mean that the implementation of LALR(1) algorithms in YAPB is done in an optimized way. :)

However, for the C11 paser specification, YAPB was abnormally terminated in the middle of LALR(1) automation production. Precisely speaking, there was a space leak in the implementation of constructing LALR(1) items from LR(0) items with spontaneous lookaheads and lookahead propagation. 

 - For a technical account for the construction algorithm, you may refer to the Dragon book (Section 4.7.5 Efficient Construction of LALR Parsing Tables, 2nd Edition)

Simply speaking, LALR(1) items have lookaheads while LR(0) items do not have ones. While LALR(1) items could be constructed from LR(1) items, the construction of LR(1) items demand much more space. A noble idea is to construct LALR(1) items from LR(0) items, which are much smaller than LR(1) items. 

Roughly, LR(0) items become LALR(1) items when proper lookaheads are added to them. Here the ideas of spontaneous lookaheads and lookahead propagation are used. 

The reason for the space leak was a bit surprising. After my implementation constructs an initial LALR(1) items with spontaneous lookaheads, it has to add more lookaheads using the lookahead propagation. In the previous implementation,

let   newLookaheads = if some condition is satisfied

                                      then propagatedLookaheds else []

in    existingLookaheads ++ newLookaheads

This code has a space leak because even when no propagated lookaheads are added, it has to have (... ++ ...) lazily! Moreover, the propagated lookaheads may be already contained in the existing lookaheads. Then the space leak will be more larger. (The duplicated lookaheads are eliminated in a later stage.)

So, I have changed this code into a new one as:

if some condition is satisfied

then accumLks propagatedLookaheds existingLookaheads else existingLookaheads

accumLks [] lookaheads = lookaheads

accumLks (lk:lks) lookaheads

  | lk `elem` lookaheads = accumLks lks lookaheads

  | otherwise = accumLks lks (lk : lookaheads)

After the change, there is no more (++) operations being accumulated, and there is no more duplicate addition of lookaheads.  

In an LALR(1) automation construction with the C11 parser specification, the new version takes only about 2GB memory while the previous leaked version took more than 16GB, which is the size of the memory in my Laptop.

3. How I was able to find the space leak problem

I've found this space leak by running a C11 parser using YAPB in parallel with viewing memory and swam usages ( available in Ubuntu)

With the C11 parser, I had added  a series of 'putStrLn's to print intermediate results from the beginning. For example, it was fine until it prints LR(0) items. There was no noticeable rise in the memory usage. After that, computing and printing spontaneous lookaheads from the LR(0) items were fine. Also, computing and printing a lookahead propagation relation was good. I still did not see any memory usage problem. 

The next step was to compute LALR(1) kernel items from LR(0) items with the spontaneous lookaheads and the lookahead propagation relation. I added a putStrLn to print the result, LALR(1) kernel items. After running this, there was a series of rising patterns in the memory usage from 2GB (the initial memory occupancy) to 16GB (the size of the laptop RAM memory) and the program was killed abnormally by the operating system. This was why I realized that there is a space leak in the stage of computing LALR(1) kernel items!

After that, I reviewed the relevant Haskell program line by line, and, very luckily, found out the space leak explained above. 

4. In retrospect

Actually, I have tried to apply the GHC profiling utility in the beginning, but it was in vain. The reason is that the abnormal terminal doesn't seem to produce a profiling result file properly. There could be my mistake in using the GHC profiling tool because I am not so familiar with it. If you have any suggestion, please leave your message. 

Anyway, I hope this article may give you a hint on how to find and fix a space leak in your Haskell programs!

On Haskell layout rule

Layout rule in Haskell allows programmers to omit writing braces and semicolons in let, where and do by a lexer and a parser who insert them automatically. Here are some references for Haskell layout rule:

• Section 2.7 for informal introduction and an example of the layout rule.
• Section 10.3 in Haskell 2010 language report. 

When I read through the sections, I feel that the layout rule is quite intuitive but its formal description is a bit difficult to understand. So, I have decided to try to explain the formal description by example so that I can understand it better, which is the purpose of this article.

Suppose a simple Haskell program as follows.

1:module Main where

2:

3:main = do

4:    putStr hello

5:    putStrLn world

6:  where

7:    hello = "Hello"

8: 

9:world = " World!!"

GHC will automatically translate it into one in the following. 

1:module Main where

2: 

3:{main = do

4:    {putStr hello

5:    ;putStrLn world

6:  }where

7:    {hello = "Hello"

8: 

9:};world = " World!!"

0:}

This is a very useful feature for programmers. However, the compiler writers will be more burdensome because the implementation of the layout rule is quite tricky. The layout rule demands a lexer and a parser to work together. You can never develop a standalone Haskell lexer correctly without support by any parsers. 

• "How does GHC implement layout?' in ghc-dev by Alexis King
• An answer by Simon Marlow in the mail thread

In this article, let me try to explain this layout rule by showing a running example of the layout translation function in the Haskell 2010 language report. This function explains the layout rule by translating one using the layout rule into another with explicit braces and semicolons (so without using the layout rule). 

L (tokens, indentations) = tokens' where

• tokens : indentation sensitive tokens
• indentations : nested indentation context (e.g., [5, 1])
• tokens' : indentation insensitive tokens using explicit braces and semicolons

To recognize spaces in Haskell lexer, special tokens <n> and {n} are introduced. 

• Firstly, {n} indicates that there is no { right after let, where, do, or of. The integer, n, is the column (indentation) of the next lexeme. It is defined as 0 when there is no lexeme and the end of file is reached. 
• Secondly, <n> indicates that there are only white spaces in front of a lexeme in a line. The integer, n, is the column (indentation) of the lexeme. 

Note that the first column is 1, not 0. The zero as an indentation is used specially, which will be explained later.

The definition of L function in Section 10.3 is as follows. 

(Group 1)

L (<n>: ts) (m : ms) 

  = ; : (L ts (m : ms))    if m = n

  = } : (L (< n >: ts) ms) if n < m

L (<n>: ts) ms = L ts ms

(Group 2)

L ({n} : ts) (m : ms) = { : (L ts (n : m : ms))  if n > m 

L ({n} : ts) []       = { : (L ts [n])           if n > 0

L ({n} : ts) ms       = { : } : (L (<n>: ts) ms)

(Group 3)

L (} : ts) (0 : ms) = } : (L ts ms)

L (} : ts) ms       = parse-error

L ({ : ts) ms       = { : (L ts (0 : ms))

(Group 4)

L (t : ts) (m : ms) = } : (L (t : ts) ms)  if m /= 0 and parse-error(t)

L (t : ts) ms = t : (L ts ms)

(Group 5)

L [ ] [] = []

L [ ] (m : ms) = } : L [ ] ms if m /= 0

For readability, I suggest to group similar rules as above. 

With the Haskell example, the L function will be explained. We start with

L (module : Main : where : ..., []) 

 = module : L (Main : where :..., [])

 = module : Main : L (where :..., [])

 = module : Main : where : L (..., [])

By 2nd rule of Group 2 since there is no { after where and before main and also main is in the first column i.e., n=1, 

 = module : Main : where : L ({1} : main : = : do : ..., [])

 = module : Main : where : { : L (main : = : do : ..., [1])

 = module : Main : where : { : main : L (= : do : ..., [1])

 = module : Main : where : { : main : = : L (do : ..., [1])

 = module : Main : where : { : main : = : do : L (..., [1])

By the same reason as above but with 1st rule of Group 2 since the indentation context [1] is not empty,

 = module : Main : where : { : main : = : do : L ({5} : putStr : hello : ... , [1])

 = module : Main : where : { : main : = : do : { : L (putStr : hello : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : L (hello : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : L (... , [5,1])

This time it is <5>, not {5} since the lexeme processed just before is an identifier hello, not a keyword, such as do or where. So, we insert ; by applying 1st rule of Group 1.  

 = module : Main : where : { : main : = : do : { : putStr : hello : L (<5> : putStrLn : world : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : L(putStrLn : world : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : L(world : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : L(... , [5,1])

Since n=3<5=m, we insert } by applying 2nd rule of Group 1. 

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : L(<3> : where : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : L(<3> : where : ... , [1])

Now the 3rd rule of Group 1 is applied to remove <3>. Note that the side conditions of the 1st and 2nd rules are not satisfied. 

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : L(where : ... , [1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : L(where : {5} : hello : = : "world" : ... , [1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : L({5} : hello : = : "world" : ... , [1])

By applying 1st rule of Group 1, 

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : L(hello : = : "world" : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : L(= : "world" : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : L("world" : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "world" : L(... , [5,1])

By applying 2nd rule of Group 1,

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : L(<1> : world : = : " world!!" : ... , [5,1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  L(<1> : world : = : " world!!" : ... , [1])

By applying 1st rule of Group ,

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : L(world : = : " world!!" : ... , [1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : world : L(= : " world!!" : ... , [1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : world : = : L(" world!!" : ... , [1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : world : = : " world!!" : L(... , [1])

Now we arrive at the end of file. By applying 2nd rule of Group 5, 

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : world : = : " world!!" : L([] , [1])

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : world : = : " world!!" : } : L([] , [])

We finish by applying 1st rule of Group 5:

 = module : Main : where : { : main : = : do : { : putStr : hello : ; : putStrLn : world : } : where : { : hello : = : "hello" : } :  ; : world : = : " world!!" : } : []

This is how we've got the layout insensitive version of the program!

We have several rules that have not been used in the running example. 

• 3rd rule of Group 2
• Three rules of Group 3
• 1st rule of Group 4

Wait, did we use 2nd rule of Group 4? Yes, we did where we consume lexemes that are not actually relevant to the layout rule, for example, as in:

L (module : Main : where : ..., []) 

 = module : L (Main : where :..., [])

The 3rd rule of Group 2 is used in a corner case that there is a use of where but is followed by nothing (i.e., EOF). In the case, we just use write { and } after the keyword where. 

The three rules of Group 3 handle programs that use braces explicitly. Let us start with the 3rd rule of Group 3. When there is an explicit opening brace, this brace is produced as it is. Importantly, the indentation context now has zero in the head position indicating the presence of an explicit opening brace.

Note that explicit braces written by programmers cannot be matched against implicit braces that are inserted by the layout rule. When there were such a case, a parse error would be issued. That is done by 1st and 2nd rules of Group 3.

In 1st rule of Group 3, an explicit closing brace is matched against the head indentation, which must be zero. Otherwise, in 2nd rule of Group 3, there is a parse error. 

The 1st rule of Group 4 is most interesting (and also problematic since this rule demands a lexer to be quite tightly coupled with a parser). Let us consider another Haskell example:

let x = 1 in x

which is expected to be translated into

let {x = 1 }in x

Let us start with 

L( let :  {5} : x : = : 1 : in : x : [], [])

 = let : L({5} : x : = : 1 : in : x : [], [])

 = let : { : L(x : = : 1 : in : x : [], [5])  

 = let : { : x : L(= : 1 : in : x : [], [5])  

 = let : { : x : = : L(1 : in : x : [], [5])  

 = let : { : x : = : 1 : L(in : x : [], [5])  

At this moment, the Haskell parser will give rise to a parse error because of the absence of a matching closing brace against the opening one inserted by the Haskell lexer. Also, note that m is 5, which is not zero. 

By applying 1st rule of Group 4, we can managed to overcome this parse error as:

 = let : { : x : = : 1 : } : L(in : x : [], [5])  

 = let : { : x : = : 1 : } : in : L(x : [], [])  

 = let : { : x : = : 1 : } : in : x : L([], [])  

 = let : { : x : = : 1 : } : in : x : []

This is what Haskell layout rule is! 

This exercise have helped me better understand the Haskell layout rule. I hope it will help you too if you are not familiar with the formal description of Haskell layout rule.  And, I will welcome any comments or corrections on this article. 

  

How to set up a HTTPS server using cohttp (in O'Caml)

Here is a short tutorial on how to set up a HTTPS server written in O'Caml using cohttp. 

Basically, there is a tutorial on writing a HTTP server in the cohttp package that we start with:

• https://github.com/mirage/ocaml-cohttp

Step I. You prepare a certificate file and a key file using opensl as:

   $ openssl genrsa -out key.pem

   $ openssl req -new -key key.pem -out csr.pem

   $ openssl x509 -req -days 9999 -in csr.pem -signkey key.pem -out cert.pem

   $ rm csr.pem

Step II. You write a server using cohttp with HTTPS mode. 

As a mode for creating a server, 

• `TCP (`Port 8000) for HTTP
• `TLS (`Crt_file_path "cert.pem", `Key_file_path "key.pem", `No_password, `Port 8000) for HTTPS

where the port number, file names, and password can be changed for your own purpose. 

$ vi server.ml

#use "topfind";;

#require "lwt";;

#load "unix.cma";;

#load "threads.cma";;

#require "cohttp-lwt-unix";;

open Lwt

open Cohttp

open Cohttp_lwt_unix

let server =

  let callback _conn req body =

    let uri = req |> Request.uri |> Uri.to_string in

    let meth = req |> Request.meth |> Code.string_of_method in

    let headers = req |> Request.headers |> Header.to_string in

    ( body |> Cohttp_lwt.Body.to_string >|= fun body ->

      Printf.sprintf "Uri: %s\nMethod: %s\nHeaders\nHeaders: %s\nBody: %s" uri

        meth headers body )

    >>= fun body -> Server.respond_string ~status:`OK ~body ()

  in

  (* [HTTP] *)

  (*   Lwt_main.run ( Server.create ~mode:(`TCP (`Port 8000)) (Server.make ~callback ())) *)

  (* [HTTPS] *)

  Lwt_main.run ( Server.create ~mode:(`TLS (`Crt_file_path "cert.pem", `Key_file_path "key.pem", `No_password, `Port 8000)) (Server.make ~callback ()))

Step III. Run

$ ocaml -I +threads server.ml

In case you meet errors such as undefined things, you may need to install some packages as:

 $ opam install cohttp-lwt-unix cohttp-async tls lwt

Modular Happy Packages

I am so happy to find modular Happy packages. 

Happy is a parser generator system for Haskell, similar to the tool Yacc for C, OCamlYacc for OCaml, and so on. It has been used for generating a GHC's Haskell parser. 

Since its birth, it has been a monolithic architecture. Now it is time to make it modular so that Happy can be used more than just GHC's Haskell parser. 

- [PR] Modularize happy #191

- piknotech/happy{modularization branch}

It consists of happy-{frontend,middleend,backend,core,test} packages. Happy-frontend is for reading .y files and parsing them into the Grammar datatype. Happy-middleend applies LR/GLR parsing algorithms to the grammar to have action tables and goto tables. Happy-backend generates template-based Haskell code using these tables. Happy-core defines common interfaces among these packages, and Happy-test is about a testing framework. It is said to have the same CLI as the original monolithic Happy so that the transition from the existing one to this one can be as smooth as possible. Isn't it great?

This is how to install this modular Happy packages in modular_happy directory.

$ mkdir modular_happy; cd modular_happy

$ git init

$ git remote add origin https://github.com/piknotech/happy

$ git pull origin modularization 

(You don't have to build it for now.)

You can test these packages with GHC's Parser:

- Parser.y

Just to read this Parser.y and to print it in Grammar datatype, this simple program is enough.

$ stack new example; cd example       (Assume example and modular_happy are in the same level)

(Include the following in package.yaml)

dependencies:

- base >= 4.7 && < 5

- happy-frontend >= 1.21.0

- happy-middleend >= 1.21.0

- happy-backend >= 1.21.0

- happy-core >= 1.21.0

(Include the following in stack.yaml)

packages:

- .

- ../modular_happy/packages/frontend

- ../modular_happy/packages/middleend

- ../modular_happy/packages/backend

- ../modular_happy/packages/core

(Edit app/Main.hs as this)

module Main where

import Happy.Frontend.CLI

import Happy.Core.Grammar

main :: IO ()

main = do

  either <- parseAndRun [] "Parser.y" "Parser"

  case either of

    Left error -> putStrLn error

    Right grammar -> putStrLn $ show $ grammar

    

$ stack build

(Download the Parser.y into the top-level directory of stack project)

$ stack exec example-exe

(It will be able to read Parser.y and to print it.)

Yeah!!

Note: If you have a build error, it might be caused by the absence of alex and happy in your system.

 - sudo apt-get install alex happy

(Special thanks to the author of the modular Happy packages, David Knothe.)

On 25 March 2023, David Knothe's proposal seems to be gradually accepted to Happy as:

 - https://github.com/haskell/happy/pulls?q=is%3Apr+author%3Aknothed+is%3Aclosed

GHCUP for managing GHC versions

GHCUP for managing GHC versions 

- https://qfpl.io/posts/multiple-ghcs-ghcup/

When I develop a Haskell project, I use Stack. But some Haskell projects that I am interested in rely on Cabal (BTW, I am still confused by cabal-install, which is a Haskell package name, or by cabal, which is a command-line. Refer to [1]). 

Alex and Happy are such projects. For those who do not know what they are, Alex is a lexical analyzer tool, and Happy is a syntax analyzer tool. Both of them have their own specification languages and after some processing, they produce a Haskell program that do the analysis. 

For some reason, I wanted to build these two projects from source. This required me to install GHC (including cabal). If I use Stack, GHC is automatically downloaded when a project is built just by a command-line, stack build. If I use Cabal, it doesn't seem to be so. I need to install GHC by myself. This is where GHCUP helps me very much. 

Build systems, package installers, and package managers seem to be a huge obstacle to Haskell beginners such as myself. 

[1] Repeat after me: "Cabal is not a Package Manager"

   : https://ivanmiljenovic.wordpress.com/2010/03/15/repeat-after-me-cabal-is-not-a-package-manager/

How to build GHCJS

This is a story of buidling GHCJS in Ubuntu 20.04. The GHC version that GHCJS depends on is 8.6.x. 

 -  https://github.com/ghcjs/ghcjs

Preliminaries: 

 - Download GHC8.6.x binary and Cabal-3.2.0.0 binary in a path accessible by PATH

    : https://www.haskell.org/ghc/download.html

    : https://www.haskell.org/cabal/download.html

 - Install alex and happy by sudo apt-get install alex happy

(According to the Happy web site, the source of happy should be installed by git clone and cabal install happy but it failed due to a reason that I do not know. It seems that building the happy source needs a happy binary. :) If you have any hint, please leave me a message.)

(During the installation of ghc-8-6-x, you may need to install libtinfo.so.5, which is available by sudo apt-get install libtinfo.)

Now you follow the GHCJS installation instruction

1. Getting and preparing the source tree

 - git clone --branch ghc-8.6 https://github.com/ghcjs/ghcjs.git

 - cd ghcjs

 - git submodule update --init --recursive

 - ./utils/makePackages.sh

(You may need to install autoconf by sudo apt-get install autoconf before you run the shell script.)

2. Building the compiler

 - cabal new-configure (When cabal new-configure was failed, you may try cabal configure, but this may be due to some cabal version problem.)

 - cabal new-build  (When cabal new-build was failed, you may try cabal build, but this may be also due to the version problem.)

 (You may need sudo apt-get install libtinfo-dev when the build fails due to the absence of libtinfo.)

It will take long time...

 - cd $YOURBIN

  (I assume that the path $YOURBIN is accessible by $PATH.)

 - ln -s $GHCJSHOME/utils/dist-newstyle-wrapper.sh ghcjs

 - ln -s $GHCJSHOME/utils/dist-newstyle-wrapper.sh ghcjs-pkg

 - ln -s $GHCJSHOME/utils/dist-newstyle-wrapper.sh haddock-ghcjs

 - ln -s $GHCJSHOME/utils/dist-newstyle-wrapper.sh hsc2hs-ghcjs

 - ln -s $GHCJSHOME/utils/dist-newstyle-wrapper.sh ghcjs-boot

 - ln -s $GHCJSHOME/utils/dist-newstyle-wrapper.sh ghcjs-run

 (There is no instruction about ghcjs-run but I attempted to add it after I found a ghcj-run-not-found error on ghcjs-boot in the next stage.)

3. Booting GHCJS

 (You may need node by sudo apt-get install nodejs, and npm by sudo apt-get install npm.)

 - ghcjs-boot --no-haddoc -no-prof -s ./lib/boot

 (In the specified directory, boot.yaml exists. Without -s option, it will get stuck with a boot.yaml-not-found error. The default instruction was without the option. I am wondering when the default one would work. )

(--no-haddoc is given as an option not to get an error, "Haddock's resource directory does not exist!")

It will take long time again...

(Umm... Sorry I switched to Miso who is a layer on top of GHCJS. You don't have to get tangled with the installation of GHCJS any more.)

How to use a personal library in another project with Stack? (Haskell)

In Haskell, Haskell tool stack is quite difficult at least to me. For example, I want to use a personal library (a pre-release version of a Hackage package) from a stack project  in another stack project. Conceptually, it is simple, but it takes a bit long to find a solution from Stackoverflow.

• Link to the relevant article in Stackoverflow

Here is a summary.

In stack.yaml, 

packages 

- '.'

- path-to-a-stack-project-directory-containing-your-personal-library

In packages.yaml, 

dependencies:

- your-personal-libary

Then run 

$ stack build

This will solve your need. How easy it is after one knows how to do it! But I worry how difficult Haskell newbies may feel. 

Switching between my office and my home working on the same working branch (Git, GitHub)

I am still a newbie to Git and GitHub. I have recently started using the notion of branches. In my office, I work on master and working branches, and I always push them to GitHub before I get back home. At my home, I work with my home computer. So I clone the GitHub repository. What I want to do is to work on the working branch and to push whatever I work on at home later.

This is what I need to do at home for this purpose.

$ git clone https://github.com/kwanghoon/polyrpc

$ cd polyrpc

$ git branch -a
* master
  remotes/origin/HEAD -> origin/master
  remotes/origin/master
  remotes/origin/working_erasure

$ git checkout origin/working_erasure
주의: 'origin/working_erasure' 체크아웃하기.

지금 'HEAD가 분리된' 상태입니다. 이 상태에서는 여기저기 돌아보고,
실험적으로 바꾸고 커밋하더라도, 체크아웃할 수 있는 다른 브랜치에
영향을 미치지 않고 변경 사항을 잃어버릴 수 있습니다.

커밋을 유지하는 브랜치를 새로 만드려면, (지금이든 나중이든) 체크아웃
명령을 다시 하면서 -b 옵션을 사용하면 됩니다. 예를 들어:

  git checkout -b <새-브랜치-이름>

HEAD의 현재 위치는 1597a06 Added some options to switch between typed and untyped runnings; Default is the typed running; Bugs in the erasure pass

$ git branch -a 

* (HEAD origin/working_erasure 위치에서 분리됨)
  master
  remotes/origin/HEAD -> origin/master
  remotes/origin/master
  remotes/origin/working_erasure

$ git checkout working_erasure

'working_erasure' 브랜치가 리모트의 'working_erasure' 브랜치를 ('origin'에서) 따라가도록 설정되었습니다.

새로 만든 'working_erasure' 브랜치로 전환합니다

$ git branch

  master

* working_erasure

$

Another quick guide for Haskell Stack

When you have Main.hs with no stack project, how can you build and run it?

In old days, I used Hugs or GHCi just to load a single Haskell file without any fancy project configurations. Sometimes the Haskell file required me to install some extra libraries such as network. Then I had only to give Hugs or GHCi an option to inform it of a  path where the libraries reside. 

How can you do this with Haskell Stack? This is the topic of this article. I found out it is easy!

$ ls 

Main.hs

$ stack init

$ stack ghci --no-load

Prelude> :l Main

Main.hs:3:1: error:

          Could not find module 'Network.Socket'

...

Prelude>:q

$ stack install network

$ stack ghci --no-load

Prelude> l: Main

Ok, one module loaded.

*Main>

This is it!! Isn't it surprisingly simple? But why does nobody explain it to me? :)

How to count the number of lines of code?

How to count the number of lines of code?

You can do it simply by combining a few Linux tools. Suppose you are in a root directory that contains many recursive subdirectories and have Haskell (.hs) source files.

$ find . -name "*.hs" -exec wc \{\} \; | cut -c 1-8 | awk 'BEGIN {sum=0} {sum=sum+$0} END {print sum}'

END.

A quick guideline on Haskell projects using stack

This is a quick guideline on Haskell projects using stack.

1. How to build a new project and to run it

 - stack new myproject
 - cd myproject
 - stack build myproject
 - stack exec myproject-exe


2. How to load the new project onto Visual Studio code

 - stack build intero

 - code .

3. How to load the project onto GHCi

 - stack ghci

How to build the Elm platform from the source on Windows.

This is a brief guideline to explain how to build the Elm platform on Windows from its source. The guideline is based on the original instruction from https://github.com/elm-lang/elm-platform.

1. Preliminaries

1.1 GHC and Cabal

This is for building Elm 0.18 from the source code. It demands GHC 7.10.x and Cabal >=1.1.8, which can be downloaded from

 - https://www.haskell.org/ghc/download.html
 - https://www.haskell.org/cabal/download.html

 For my Windows 10 on x86_64, I downloaded GHC 7.10.3 and Cabal 2.2.0.0.

After downloading the two packages, you first unpack the GHC package into a directory named, say, C:\work\ghc. The unpacking the packages resulted in directory ghc-7.10.3 including

 - C:\Work\ghc\ghc-7.10.3\bin

After unpacking the Cabal package, you will simply get cabal.exe. Then copy the Cabal executable into the GHC binary directory mentioned above.

Then set path to include the GHC binary directory. Test it by opening a Dos terminal to run ghc --version and cabal --version.




1.2 MinGWS and msys

Install MinGWS and msys. 

 - mingw-get-setup.exe   from http://www.mingw.org/
    (to install mingw-developer-toolkit, mingw32-base, mingw32-gcc-g++, msys-base)

 - MSYS-1.0.11.exe    from http://www.mingw.org/wiki/MSYS or  http://downloads.sourceforge.net/mingw/MSYS-1.0.11.exe

You need to add the paths to the executables to your path environment.

 - C:\MinGW\bin
 - C:\msys\1.0\bin

At first, I thought the installation of MinGWS and msys is enough to make it to build Elm-Platform on Windows successfully. But it failed. Actually, I cannot explain the exact reason, but it seems to need shell script facilities to be successful. For example, I cannot execute C:\msys\1.0\bin\awk on Dos terminal. Is this because awk does not have .exe nor .bat as its extension? 


1.3 Ubuntu terminal on Windows 10

So, the next trial is to use the Ubuntu terminal on Windows, which provides shell environments. 

 - https://docs.microsoft.com/en-us/windows/wsl/install-win10

 - https://tutorials.ubuntu.com/tutorial/tutorial-ubuntu-on-windows#0


   (which will be redirectd to Microsoft App store, https://www.microsoft.com/en-us/store/p/ubuntu/9nblggh4msv6)

After your successful installation of the Ubuntu terminal on Windows 10, do launch the Ubuntu terminal from the Windows start menu. 

khchoi@LAPTOP-KE15PJ8N:/mnt/c/work/elmbuild$ ls
BuildFromSource.hs  

khchoi@LAPTOP-KE15PJ8N:/mnt/c/work/elmbuild$ df
Filesystem     1K-blocks      Used Available Use% Mounted on
rootfs         498799612 121793964 377005648  25% /
none           498799612 121793964 377005648  25% /dev
none           498799612 121793964 377005648  25% /run
none           498799612 121793964 377005648  25% /run/lock
none           498799612 121793964 377005648  25% /run/shm
none           498799612 121793964 377005648  25% /run/user
C:             498799612 121793964 377005648  25% /mnt/c

As you see above, my folder is /mnt/c/work/elmbuild where BuildFromSource.hs is. In the next, I will tell you where you can download this haskell file. 

Note that /mnt/c is a (virtual) path to the C drive on Windows viewed from the Ubuntu side.

In conclusion, you are in the directory, elmbuild, in the Ubuntu terminal.



2. Building Elm-Platform

With the Ubuntu terminal, I assume that you are in /mnt/c/work/elmbuild/. 

Then you proceed as the Elm instruction tells you:

 - curl https://raw.githubusercontent.com/elm-lang/elm-platform/master/installers/BuildFromSource.hs > BuildFromSource.hs

 - runhaskell.exe BuildFromSource.hs 0.18



Note that I installed the Window version of GHC, and so the executable files all have .exe as an extension. On the Ubuntu terminal, you must say runhaskell.exe, not runhaskell, which would be OK if you installed the Linux version of GHC. 

If you have a little fortune, you will see a bunch of logs saying cloning source codes from GitHub and building them by GHC and so on. 

The building will lead to a compilation error as follows.

Installed blaze-html-0.9.0.1
Resolving dependencies...
Notice: installing into a sandbox located at
C:\Work\elmbuild\Elm-Platform\0.18\.cabal-sandbox
Configuring elm-compiler-0.18...
Building elm-compiler-0.18...
Installed elm-compiler-0.18
Configuring elm-package-0.18...
Building elm-package-0.18...
Failed to install elm-package-0.18
Build log ( C:\Work\elmbuild\Elm-Platform\0.18\.cabal-sandbox\logs\ghc-7.10.3\elm-package-0.18-5b9PWczZoztJ6nOvjcNrfc.log ):
Preprocessing executable 'elm-package' for elm-package-0.18..
Building executable 'elm-package' for elm-package-0.18..
[ 1 of 27] Compiling Utils.Paths      ( src\Utils\Paths.hs, dist\dist-sandbox-25b26694\build\elm-package\elm-package-tmp\Utils\Paths.o )

src\Utils\Paths.hs:15:27: Not in scope: ‘N.toFilePath’

src\Utils\Paths.hs:19:26:
    Not in scope: ‘Package.versiontoString’
    Perhaps you meant one of these:
      ‘Package.versionToString’ (imported from Elm.Package),
      ‘Package.versionFromString’ (imported from Elm.Package)
cabal: Leaving directory 'C:\Work\elmbuild\Elm-Platform\0.18\elm-package'
cabal: Error: some packages failed to install:
elm-make-0.18-EdAAG7jYG0T1gF34nRbUyL depends on elm-make-0.18 which failed to
install.
elm-package-0.18-5b9PWczZoztJ6nOvjcNrfc failed during the building phase. The
exception was:
ExitFailure 1
elm-repl-0.18-CfO4RJPUoASJxV81yVDYp2 depends on elm-repl-0.18 which failed to
install.

This compilation error can be fixed by changing Line 15 and Line 19 in elm-pakcage/src/Utils/Path.hs, as follows:

  1 module Utils.Paths where
  2
  3 import System.FilePath
  4
  5 import qualified Elm.Package as Package
  6
  7 internals = "_internals"
  8
  9 libDir = "public" </> "catalog"
 10
 11 json = "docs.json"
 12 index = "index.elm"
 13 listing = "public" </> "libraries.json"
 14
 15 library name = libDir </> N.toFilePath name
    =>
    library name = libDir </> Package.toFilePath name    
 16
 17 libraryVersion :: Package.Name -> Package.Version -> FilePath
 18 libraryVersion name version =
 19         library name </> Package.versiontoString version

    =>      library name </> Package.versionToString version

Here is a patch for the change above.

diff --git a/src/Utils/Paths.hs b/src/Utils/Paths.hs
index f0752c5..e746787 100644
--- a/src/Utils/Paths.hs
+++ b/src/Utils/Paths.hs
@@ -12,9 +12,9 @@ json = "docs.json"
 index = "index.elm"
 listing = "public" </> "libraries.json"
 
-library name = libDir </> N.toFilePath name
+library name = libDir </> Package.toFilePath name
 
 libraryVersion :: Package.Name -> Package.Version -> FilePath
 libraryVersion name version =
- library name </> Package.versiontoString version
+ library name </> Package.versionToString version
 

Then rerun runhaskell BuildFromSource.hs 0.18. You will succeed in building Elm-platform.

To see it work, change your current directory to Elm-Platform/0.18/.cabal-sandbox/bin/. Then run elm-repl.exe and see a good thing as follows:

khchoi@LAPTOP-KE15PJ8N:/mnt/c/work/elmbuild/Elm-Platform/0.18$ ./.cabal-sandbox/bin/elm-repl.exe
---- elm-repl 0.18.0 -----------------------------------------------------------
 :help for help, :exit to exit, more at 
--------------------------------------------------------------------------------
> 1+1
2 : number
>

In fact, I found out that you can run elm-repl on the Dos terminal as well. 

C:\Work\elmbuild\Elm-Platform\0.18> cabal exec elm-repl
---- elm-repl 0.18.0 -----------------------------------------------------------
 :help for help, :exit to exit, more at 
--------------------------------------------------------------------------------
> 1+1
2 : number

Be careful! The first run of elm-repl may get terminated abnormally. But from the second run, it will work without any problem.

In conclusion, you build the Elm-Platform on the Ubuntu terminal, but you run it on the Dos terminal. This looks very natural on Windows 10!

Have a good luck!!

Building ghc-mod

This is a post about building ghc-mod for Haskell IDEs.

To build ghc-mod with
 - ghc-8.2.2

needs some manual editing on stack.yaml in your project generated by stack.
Here is my edit for a successful build of ghc-mod 5.9.0.0.

extra-deps: 

- https://hackage.haskell.org/package/ghc-mod-5.9.0.0/candidate/ghc-mod-5.9.0.0.tar.gz

- cabal-helper-0.8.0.0

- monad-journal-0.7.2

- optparse-applicative-0.13.2.0

- either-4.4.1.1

- extra-1.6.6

- free-4.12.4

- haskell-src-exts-1.20.1

The operating system is Mac OS High Sierra (10.13.4), but the dependencies listed above seem to be universal over other operating systems. 

LaTeX for Logicians and Programming Language People

I found a web site for a guide to write natural deduction proofs in latex. This site should not only be useful for logicians as the web site says, but it must also be useful to programming language people.

• http://www.logicmatters.net/latex-for-logicians/

Haskell on Visual Studio Code for Windows

I am happy to hear a news about Haskell support on Windows via Visual Studio Code and its extension called Haskelly. These days, my main operating system has been Windows 7 and 10. Linux is for running a web server, and Mac is for an old laptop. My students have extensively used Windows OS. For me to teach Haskell programming, I have no option but to find an appropriate IDE necessarily running on Windows. Sometime ago, I recommended Eclipse and Haskell plugin on it. Now I believe I will recommend Visual Studio Code and its extension called Haskelly for Haskell programming to my Windows-favored students.

[Haskelly]

• https://marketplace.visualstudio.com/items?itemName=UCL.haskelly

[Installation instructions]

• Install Visual Studio Code
• Run Visual Studio Code to activate the Haskelly extension
• Download a stack installer and run it
• Launch your CMD window or Windows PowerShell
• Run "stack install intero QuickCheck stack-run --install-ghc"
• stack : the name of a command for Haskell tool stack
• intero : a tool for auto-completion of names in Haskell programs
• QuickCheck : a property-based testing tool
• stack-run : an option to direct stack to compile the source codes and to run the default executable
• --install-ghc : an option to install GHC (Glasgow Haskell compiler)
• Rerun Visual Studio Code
• Open a new file named Main.hs extension to write the following
• module Main where
• main = putStrLn "Hello Haskell"
• Run it!

Note. I guess you will meet some error messages: infero does not work.  But VS code may work partially for Haskell programming, though type information is not properly displayed by infero when you hover a mouse cursor over some function.

In this error, you may try the following

• Run "stack build intero", "stack build QuickCheck", "stack build stack-run" separately. 
• It may help you to build intero and QuickCheck at least. 
• But I failed to build stack-run with an error message like "In the dependencies for unix-2.7.2.1: unbuildable must match <0, but the stack configuration has no specified version"
• I do not know what solution is available for the problem. 

Lectures on Haskell Programming

For novice learners, U. of Pennsylvania lecture, Introduction to Haskell  is good :

• https://www.seas.upenn.edu/~cis194/fall16/
• http://haskellbook.com/

• Book : Learn you a Haskell for great good
• http://learnyouahaskell.com/

Middle-level learners may be interested in S. Weirich's lecture, Advanced Programming, which teaches from basic and advanced Haskell programming :

• http://www.seas.upenn.edu/~cis552/15fa/
• with RWH book http://book.realworldhaskell.org/

For advanced learners, I recommend Bryan O'Sullivan's stanford lecture, Functional Systems in Haskell :

• http://www.scs.stanford.edu/11au-cs240h/

Excel : Mouse Wheel zooms in and out instead of scrolls

When you suddenly find out your mouse wheel make the excel worksheet zoom in and out instead of scrolling it, you can correct it by

 - File -> Option -> Advanced -> Zoon On Roll with Intellimouse

https://answers.microsoft.com/en-us/msoffice/forum/msoffice_install-mso_other/mouse-wheel-magnifies-instead-of-scrolls/40644484-e043-446d-bee6-52cbb3d4865a