Current HEAD of main fails to build

[shingarov]

Trying to build, following the README.md in the most literal way:

$ git clone --recursive https://github.com/ucsd-progsys/liquidhaskell-tutorial.git
$ stack build --fast --file-watch

ends up in the following failure:

...
Configuring liquidhaskell-tutorial-0.2.0.0...
liquidhaskell-tutorial           > build (lib)
Preprocessing library for liquidhaskell-tutorial-0.2.0.0..
Building library for liquidhaskell-tutorial-0.2.0.0..
[ 1 of 13] Compiling Paths_liquidhaskell_tutorial

**** LIQUID: SAFE (0 constraints checked) **************************************
[ 2 of 13] Compiling Tutorial_01_Introduction

**** START: pandoc *************************************************************

**** DONE:  pandoc *************************************************************

**** START: pandoc *************************************************************

**** DONE:  pandoc *************************************************************

**** LIQUID: UNSAFE ************************************************************

/home/boris/work/liquidhaskell-tutorial/src/Tutorial_01_Introduction.lhs:30:27: error:
    Liquid Type Mismatch              
    .                                 
    The inferred type                 
      VV : {v : GHC.Types.Int | v >= 0
                                && v == len xs}
    .                                 
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV /= 0}
    .                                 
    in the context                    
      xs : {v : [GHC.Types.Int] | len v >= 0}
   |                                  
30 | average xs = sum xs `div` length xs
   |                           ^^^^^^^^^

Completed 65 action(s).               

--  While building package liquidhaskell-tutorial-0.2.0.0 (scroll up to its section to see the error) using:
      /home/boris/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_3.2.0.0_ghc-8.10.1 --builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-3.2.0.0 build lib:liquidhaskell-tutorial --ghc-options " -fdiagnostics-color=always"
    Process exited with code: ExitFailure 1
Type help for available commands. Press enter to force a rebuild.

This is under the following setup:

$ cat /etc/issue
Ubuntu 21.10 \n \l
$ stack --version
Version 2.7.3, Git revision 7927a3aec32e2b2e5e4fb5be76d0d50eddcc197f x86_64 hpack-0.34.4
$ z3 --version
Z3 version 4.8.9 - 64 bit

Am I missing something obvious?

[ranjitjhala]

Hi @shingarov -- thanks for trying the tutorial!

The behavior above is as desired: there are various (refinement type errors) and your task as you work through the tutorial is to fix them.

However, it occurs to me this is in the intro chapter and there is no surrounding text/comments about fixing the error, so I should maybe make this not a code block!

[To work past this error, just comment out the average function -- but as you work through the next chapters you will see these errors that you are supposed to fix.

Does that help?

Best!

• Ranjit.

[shingarov]

The behavior above is as desired

I see; thanks!

I think it needs to be explained in the text: the current wording is very confusing. In several decades of R&D career I found there is an extremely difficult balance between on the one hand, one's own struggle-towards-understanding when working through a book, and on the other hand, the book should afford the reader a certain promise: that if the reader follows diligently -- pays attention, does all the exercises, etc -- then "everything is going to end well".

Usually in a programming tutorial, readers would expect some clear separation between a "Setup" chapter vs "here begins the actual story". After going through a bunch of apt-get install and git clone and ./configure; make and make test there comes a caesura, a restful point of satisfaction, of telling oneself: "Ok now I know the environment is set up; now I am ready to start".

I think a departure from this expectation deserves to be mentioned -- perhaps something like PR#116?

thanks for trying the tutorial!

Following through the tutorial during the past weekend has been very useful. I will be explaining liquid types to the Smalltalk community at the coming FAST conference (using my own implementation in Smalltalk, thus adding Smalltalk to the list of "Liquid types have been implemented in ML, Haskell,..."), and I am very interested in others' expository approaches to the subject.

[ranjitjhala]

Thanks very much! Yes totally agree, as the tool authors we often have “blind spots” that make us miss these crucial things. Thanks for the PR!

On Mon, Nov 8, 2021 at 7:09 AM Boris Shingarov @.***> wrote:

The behavior above is as desired

I see; thanks!

I think it needs to be explained in the text: the current wording is very confusing. In several decades of R&D career I found there is an extremely difficult balance between on the one hand, one's own struggle-towards-understanding when working through a book, and on the other hand, the book should afford the reader a certain promise: that if the reader follows diligently -- pays attention, does all the exercises, etc -- then "everything is going to end well".

Usually in a programming tutorial, readers would expect some clear separation between a "Setup" chapter vs "here begins the actual story". After going through a bunch of apt-get install and git clone and ./configure; make and make test there comes a caesura, a restful point of satisfaction, of telling oneself: "Ok now I know the environment is set up; now I am ready to start".

I think a departure from this expectation deserves to be mentioned -- perhaps something like PR#116?

thanks for trying the tutorial!

Following through the tutorial during the past weekend has been very useful. I will be explaining liquid types to the Smalltalk community at the coming FAST conference (using my own implementation in Smalltalk, thus adding Smalltalk to the list of "Liquid types have been implemented in ML, Haskell,..."), and I am very interested in others' expository approaches to the subject.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell-2Dtutorial_issues_115-23issuecomment-2D963253219&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=nGpCJ8gdNlIVfYTiXFhagqLRE0cYBNy_2hmugABzSg5awkuperSkH8Ilg_ck4gAl&s=dknyasM2-qhVWpti-WUTujeW_5qoN3QKqoFdFwgQjLc&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OCUZFFQOHORS2MM2NTUK7R37ANCNFSM5HNSYXQA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=nGpCJ8gdNlIVfYTiXFhagqLRE0cYBNy_2hmugABzSg5awkuperSkH8Ilg_ck4gAl&s=GAgzVB3SsPHVkHRIAyiiXklbvjocipCj-0HAUbxr58A&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=nGpCJ8gdNlIVfYTiXFhagqLRE0cYBNy_2hmugABzSg5awkuperSkH8Ilg_ck4gAl&s=DqYVxM7D8MGwnSbWb_fVVAKpr2TKFpccFLTp3-Q9hcE&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=nGpCJ8gdNlIVfYTiXFhagqLRE0cYBNy_2hmugABzSg5awkuperSkH8Ilg_ck4gAl&s=OrEcznSSBDAZEj3t--ft3W9fk2fbz1mxrY577FFy41Y&e=.

[shingarov]

Closing because the issue has been resolved in 8bf919a.