Re: [Haskell-cafe] install cuda
It looks like you are using Cygwin for a Unix-alike environment. For building Haskell bindings to C libraries you are better off with MinGW + MSYS. On 30 March 2013 19:43, Peter Caspers pcaspers1...@gmail.com wrote: I am trying to install the cuda package on a Windows 7 enviroment. However I run into an error and can not figure out, what it is. Can someone help ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell SBV Package with Z3
Dear L. Erkok, First I would like to wish you happy easter and I would like to thank you for your help. I have a couple of more questions. I am now playing with SBV package, however I am not sure if I understand the use of arrays, maybe you can give me some pointers. For example I want to prove the following (note: this example is only used to illustrate my question, I thought I've read somewhere in Haddock that this method only support functions with 7 parameters?) prove $ \(a :: SWord8) b c - a . b b . c == a . c Q.E.D. how should I express this using SymArray? Thanks in advance! Yours sincerely, Jun Jie 2013/3/29 Levent Erkok erk...@gmail.com Sorry, there were a couple of typos in the last example. It should read: allSat $ \(x::SWord8) - x `shiftL` 2 ./= x Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using sat/allSat as opposed to prove, and hence the inversion of equality in the property.) -Levent. On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok erk...@gmail.com wrote: You're welcome Jun Jie. Regarding getting a different counter example: That's perfectly normal. When SMT solvers build models they use random seeds. Furthermore, different versions of the same solver can use different algorithms/heuristics to arrive at the falsifying model. So, it's entirely expected that you get a different counter-example. You can turn the question around, and ask the solver to give you all counter-examples like this: allSat $ \x - \(x::SWord8) - x `shiftL` 2 .!= x -Levent. On Mar 29, 2013, at 1:42 AM, J. J. W. bsc.j@gmail.com wrote: Dear Levent, Thank you for your support. I am very honoured to have the developer of the SBV package to solve my elementary problem. I noticed that the counter-example given by my Z3 differs from the one said on HackageDB: sbv-2.10. Code that is on Hackage: Prelude Data.SBV prove $ forAll [x] $ \(x::SWord8) - x `shiftL` 2 .== x Falsifiable. Counter-example: x = 128 :: SWord8 My current GHCi output: Prelude Data.SBV prove $ forAll [x] $ \(x::SWord8) - x `shiftL` 2 .== x Falsifiable. Counter-example: x = 51 :: SWord8 (0.02 secs, 1196468 bytes) Thank you for your help! Yours sincerely, Jun Jie 2013/3/29 Levent Erkok erk...@gmail.com Hi Jun Jie: SBV uses some of the not-yet-officially-released features in Z3. The version you have, while it's the latest official Z3 release, will not work. To resolve, you need to install the development version of Z3 (something that is at least 4.3.2 or better). Here're instructions from the Microsoft folks explaining how to get these builds: http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html Let me know if you find any issues after you get the latest-development version of Z3 installed. -Levent. On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. bsc.j@gmail.com wrote: Dear all, I have a small question regarding the installation of the SBV package. I first installed the SBV 2.10 package with cabal with the following instructions: cabal install sbv Next I installed the Z3 theorem prover and adding the path to my system variables (Windows 7 x64). Next I tested whether I could find it by opening cmd.exe and then typing z3, I get an error message of Z3, so I can safely assume the system can find it. (I added the path to the bin of Z3, I have not included the include directory, I see no reason why I should add a path to this directory, but maybe I am wrong). I ran the program: SBVUnitTests. However it had some errors in the beginning and afterwards a few failures. Having no idea how to fix this, I continued to check whether I can get the SBV to work. So I started to execute the SBV package: ghci -XScopedTypeVariables ghci :m Data.SBV ghci prove $ \(x::SWord8) - x `shiftL` 2 .== 4*x Now this should return Q.E.D., however it returned the following: An error occured. Failed to complete the call to z3 Executable: C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe Options: /in /smt2 Exit code: 0 Solver output: === ; :smt.mbqi ; :pp.decimal_precision === Giving up.. It does seems like that the Z3 has a normal output, however not a result. Can someone help me to figure out what I actually did wrong? I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2 Thank you for your help! Yours sincerely, Jun Jie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Threadscope 0.2.2 goes in segmentation fault on Mac Os X 10.8.3
Fair enough :) Here is the gdb output: (gdb) run Starting program: /Users/adinapoli/Library/Haskell/ghc-7.6.2/bin/threadscope Reading symbols for shared libraries ++... done Reading symbols for shared libraries . done Reading symbols for shared libraries . done Reading symbols for shared libraries . done Reading symbols for shared libraries . done Program received signal EXC_BAD_ACCESS, Could not access memory. Reason: KERN_INVALID_ADDRESS at address: 0x 0x in ?? () I have two hypothesis: a) could be the RAM (tips about some RAM testing tool?) b) could be some programs which is writing in that portion of memory, see: https://discussions.apple.com/thread/3734077?start=0tstart=0 On 30 March 2013 15:19, John Wiegley jo...@fpcomplete.com wrote: Alfredo Di Napoli alfredo.dinap...@gmail.com writes: I know it's a bit difficult to debug this way, I can try debugging with gdb if it can help. Yes, can you show us a backtrace from gdb, and also look in your CrashReports log folder to see if it gives a bit more information on the state of the process at the time it died? Thanks, -- John Wiegley FP Complete Haskell tools, training and consulting http://fpcomplete.com johnw on #haskell/irc.freenode.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
Hi, thank you. I could resolve some of the problems by removing spaces from the Cuda and Haskell platform installation paths. Now I am left wiht the following error: configure:3596: checking for library containing cuDriverGetVersion configure:3627: c:\HaskellPlatform\2012.4.0.0\mingw\bin\gcc.exe -o conftest.exe -Wl,--hash-size=31 -Wl,--reduce-memory-overheads -I/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/include -L/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/lib conftest.c 5 C:\Users\Peter\AppData\Local\Temp\ccOsnsjD.o:conftest.c:(.text+0xc): undefined reference to `cuDriverGetVersion' collect2: ld returned 1 exit status In fact the library path -L/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/lib is not correct (there are two subfolders x64 and Win32 containing the lib files) and I do not see where this path is actually taken from. I defined an enviroment variable LD_LIBRARY_PATH with the correct paths (separated by a colon), but it seems to be ignored. Also copying the lib files to the path I see in the log does not help. Do you have any hint for me concerning this ? Peter Am 31.03.2013 00:56, schrieb Henk-Jan van Tuyl: On Sat, 30 Mar 2013 20:43:58 +0100, Peter Caspers pcaspers1...@gmail.com wrote: Hi, I am trying to install the cuda package on a Windows 7 enviroment. However I run into an error and can not figure out, what it is. : : configure: error: C compiler cannot create executables See `config.log' for more details : The message says it all: See `config.log' for more details The config.log file is probably in the directory where cabal-install unpacks it (%appdata%\cabal\cuda-revision); you can also use the commands: cabal unpack cuda cd cuda cabal install notepad config.log I just had the same error message for another package; from the config.log file it became clear, that the linker could not find the necessary library. Make sure, that the libraries and header files can be found by the compiler and linker, by setting the proper environment variables, see [0] Regards, Henk-Jan van Tuyl [0] http://www.haskell.org/haskellwiki/Windows#Tools_for_compilation ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Threadscope 0.2.2 goes in segmentation fault on Mac Os X 10.8.3
Alfredo Di Napoli alfredo.dinap...@gmail.com wrote: Fair enough :) Here is the gdb output: (gdb) run Starting program: /Users/adinapoli/Library/Haskell/ghc-7.6.2/bin/threadscope Reading symbols for shared libraries ++... done Reading symbols for shared libraries . done Reading symbols for shared libraries . done Reading symbols for shared libraries . done Reading symbols for shared libraries . done Program received signal EXC_BAD_ACCESS, Could not access memory. Reason: KERN_INVALID_ADDRESS at address: 0x 0x in ?? () That's a NULL-pointer exception. I have two hypothesis: a) could be the RAM (tips about some RAM testing tool?) b) could be some programs which is writing in that portion of memory Definitely an application error. NULL is never a valid memory address. Missing NULL-pointer checks are a very common error source in low level programming. What do you mean by _some_ program? It's the program that you started (threadscope). Tobi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
On Sun, 31 Mar 2013 17:03:22 +0200, Peter Caspers pcaspers1...@gmail.com wrote: In fact the library path -L/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/lib is not correct (there are two subfolders x64 and Win32 containing the lib files) and I do not see where this path is actually taken from. I defined an enviroment variable LD_LIBRARY_PATH with the correct paths (separated by a colon), but it seems to be ignored. Also copying the lib files to the path I see in the log does not help. The environment variable should probably be LIBRARY_PATH; I use a semicolon as separator. See also LD_LIBRARY_PATH vs LIBRARY_PATH[0]. Regards, Henk-Jan van Tuyl [0] http://stackoverflow.com/questions/4250624/ld-library-path-vs-library-path -- http://Van.Tuyl.eu/ http://members.chello.nl/hjgtuyl/tourdemonad.html Haskell programming -- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
Try my fork: https://github.com/mainland/cuda In particular, read WINDOWS.md. Geoff On 03/31/2013 07:54 AM, Stephen Tetley wrote: It looks like you are using Cygwin for a Unix-alike environment. For building Haskell bindings to C libraries you are better off with MinGW + MSYS. On 30 March 2013 19:43, Peter Caspers pcaspers1...@gmail.com wrote: I am trying to install the cuda package on a Windows 7 enviroment. However I run into an error and can not figure out, what it is. Can someone help ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
The environment variable should probably be LIBRARY_PATH; I use a semicolon as separator. See also LD_LIBRARY_PATH vs LIBRARY_PATH[0]. yes, it's LIBRARY_PATH. The x64 version of cuda.lib is not recognized at all (same error message as if the file was not existent). The Win32 version works, but results in configure:3627: c:\HaskellPlatform\2012.4.0.0\mingw\bin\gcc.exe -o conftest.exe -Wl,--hash-size=31 -Wl,--reduce-memory-overheads -I/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/include -L/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/lib conftest.c -lcuda 5 C:\Users\Peter\AppData\Local\Temp\ccOwCQ6n.o:conftest.c:(.text+0xc): undefined reference to `cuDriverGetVersion' collect2: ld returned 1 exit status I ran nm on cuda.lib and got the entry nvcuda.dll: I .idata$4 I .idata$5 I .idata$6 T .text U _IMPORT_DESCRIPTOR_nvcuda I _imp__cuDriverGetVersion@4 T cuDriverGetVersion@4 this looks ok so far. Running nm on the x64 version of the lib file results in rubbish output (consistent with the observation above). I understand that LD_LIBRARY_PATH is used to look up to dll when running the program (is that correct?). However we are not at this point yet, are we, since the error occurs on the gcc invocation ? Try my fork: https://github.com/mainland/cuda In particular, read WINDOWS.md. I also read Geoffreys WINDOWS.md and understood that configuring dll names are only necessary when using ghci, not for compiled programs (nothing to do for this case ?) and in particular not for installing the package ? Actually the dll is not named nvcuda.dll as indicated in the nm output, but rather cudart32_41_28.dll I suppose and this file is located in the bin subfolder. I should set LD_LIBRARY_PATH to the bin folder, yes ? Should I configure this dll name for package installation already (i.e. in addition to what is mentioned in WINDOWS.md) ? If yes, how ? Thank you Peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
On 03/31/2013 05:55 PM, Peter Caspers wrote: The environment variable should probably be LIBRARY_PATH; I use a semicolon as separator. See also LD_LIBRARY_PATH vs LIBRARY_PATH[0]. yes, it's LIBRARY_PATH. The x64 version of cuda.lib is not recognized at all (same error message as if the file was not existent). The Win32 version works, but results in configure:3627: c:\HaskellPlatform\2012.4.0.0\mingw\bin\gcc.exe -o conftest.exe -Wl,--hash-size=31 -Wl,--reduce-memory-overheads -I/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/include -L/c/CUDA/NVIDIA_GPU_Computing_Toolkit/CUDA/v4.1/lib conftest.c -lcuda 5 C:\Users\Peter\AppData\Local\Temp\ccOwCQ6n.o:conftest.c:(.text+0xc): undefined reference to `cuDriverGetVersion' collect2: ld returned 1 exit status I ran nm on cuda.lib and got the entry nvcuda.dll: I .idata$4 I .idata$5 I .idata$6 T .text U _IMPORT_DESCRIPTOR_nvcuda I _imp__cuDriverGetVersion@4 T cuDriverGetVersion@4 this looks ok so far. Running nm on the x64 version of the lib file results in rubbish output (consistent with the observation above). You're using a version of GHC that targets 32-bit x86, so the 64-bit library is not going to do you any good. cuDriverGetVersion@4 is the stdcall-mangled version of cuDriverGetVersion. The CUDA headers (at least in the 5.0 toolkit) do not properly declare all CUDA functions as stdcall under gcc, even though they are. This is why you get an undefined reference---gcc see cuDriverGetVersion' declared ccall in the header, so it looks for the wrong symbol. I would guess that the 4.1 toolkit has this same problem the same. In general, there is no support for using the CUDA SDK with the mingw tools. I hacked around this enough to get it to work for the driver API, but you have to use my fork. I understand that LD_LIBRARY_PATH is used to look up to dll when running the program (is that correct?). However we are not at this point yet, are we, since the error occurs on the gcc invocation ? Try my fork: https://github.com/mainland/cuda In particular, read WINDOWS.md. I also read Geoffreys WINDOWS.md and understood that configuring dll names are only necessary when using ghci, not for compiled programs (nothing to do for this case ?) and in particular not for installing the package ? There's more to it than reading my WINDOWS.md. If you want to build the cuda package at all, you also need to use my fork. Actually the dll is not named nvcuda.dll as indicated in the nm output, but rather cudart32_41_28.dll I suppose and this file is located in the bin subfolder. I should set LD_LIBRARY_PATH to the bin folder, yes ? Should I configure this dll name for package installation already (i.e. in addition to what is mentioned in WINDOWS.md) ? If yes, how ? There are two dlls you need. nvcuda.dll corresponds to libcuda on Linux, and its .lib file on Windows is cuda.lib. cudart32_41_28.dll corresponds to libcudart on Linux, and its .lib file on Windows is cudart.lib. You will need them both. I was able to install the cuda package under 32-bit GHC 7.4.2 using the 5.0 SDK and use it from within ghci. This required using my fork of the cuda repo and following the instructions in my WINDOWS.md. Make sure nvcc is in your path (the CUDA installer should have made this so) and try 'cabal configure'. LD_LIBRARY_PATH is used on most UNIX flavors. I don't believe it does anything in Windows. You will instead need to modify your Path environment variable from the System Settings-Advanced System Settings control panel. Geoff ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Threadscope 0.2.2 goes in segmentation fault on Mac Os X 10.8.3
Hi Tobias, What do you mean by _some_ program? It's the program that you started (threadscope). In a forum I've read that this error could be some third party app (for example one started at login or running as a daemon) which is conflicting and causing the error. Unlikely, but i've reported the possibility for completeness. Said that,has someone had any luck in running Threadscope on Mac OS X 10.8 at all? Thanks, A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
yes I more or less saw this in the meantime, too. Actually modifying the
source code on which the error is reported from
configure: failed program was:
| /* confdefs.h */
| #define PACKAGE_NAME Haskell CUDA bindings
| #define PACKAGE_TARNAME cuda
...
| #ifdef __cplusplus
| extern C
| #endif
| char cuDriverGetVersion ();
| int
| main ()
| {
| return cuDriverGetVersion ();
| ;
| return 0;
| }
to (for example)
#include stdlib.h
#include stdio.h
#include string.h
#include cuda.h
int
main( int argc, char** argv)
{
int driverVersion = 0;
cuDriverGetVersion(driverVersion);
printf(version = %d\n,driverVersion);
return 0;
}
let me compile, link and run without errors. Alright, got it now, I will
try your github. Do you think it works with CUDA 4.1 ? On my laptop this
is the latest version that runs due to the card driver.
Thanks in any case
Peter
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Specialized Computer Architecture - A Question
And if you are, you may be interested in https://github.com/tommythorn/Reduceron The underlying topic is a fascinating one. The fact that people ignore is that silicon cycle time improvements have been fairly modest - perhaps 2-3 orders of magnitude and we have long been at the point where wire delays are what matters. Without significant innovation, silicon scaling would just have given you a moderately faster cpu, but ridiculously tiny. Those innovations are countless, pipelining, caches, superscalar, out-of-order, speculation, ... Now that conventional single-threaded performance is peaking out, the time is ripe to revisit functional machines and apply these innovations. Reduceron is an amazing accomplishment (do and there are other projects in this space too. I hope the research on this continues. My only contribution here is to try to expand the usefulness of Reduceron and get it running on cheaper hardware. I would love more contributors, especially on compiler side (using a real Haskell front-end would be just lovely). Anyway, check it out and play around. I'll be happy to help. Tommy Thorn On Mar 19, 2013, at 05:07 , Simon Farnsworth si...@farnz.org.uk wrote: OWP wrote: Ironically, you made an interesting point on how Moore's Law created the on chip real estate that made specialized machines possible. As transistor sizing shrinks and die sizes increase, more and more real estate should now be available for usage. Oddly, what destroyed specialized machines in the past seemed to be the same cause in reviving it from the dead. The ARM Jazelle interface - I'm not familiar with it's but it's got me curious. Has there been any though (even in the most lighthearted discussions) on what a physical Haskell Machine could look like? Mainly, what could be left to compile to the stock architecture and what could be sent out to more specialized areas? You might be interested in looking at the Reduceron - http://www.cs.york.ac.uk/fp/reduceron/ - it was an FPGA-based effort to design a CPU explicitly for a Haskell-like language. -- Simon Farnsworth ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] cabal install pandoc
On Fri, Mar 29, 2013 at 08:05:47AM -0230, Roger Mason wrote: Thank you for your response. 'ghc-pkg check' shows some problems: http://pastebin.ca/2344794 On 03/28/2013 08:01 PM, Patrick Wheeler wrote: So I printed off the requirements for pandoc on a empty ghc-7.6.2 install you can find it at: http://hpaste.org/84794 I do not see any odd package versions listed in what you posted so far. No promise I will be able to help afterwards but it might help to see the full log, and then again with verbosity turned on. So seperate pastes for: * `cabal install pandoc --dry-run` * `cabal install pandoc --dry-run --verbose=2` * `cabal install pandoc --dry-run --verbose=3` You might also want to run a `ghc-pkg check` to check to see if your packages are consistent/unbroken. 'ghc-pkg check' shows some problems: http://pastebin.ca/2344794 It looks like your entire Haskell Platform installation is completely hosed. Sad to say, but I think your best bet is to simply reinstall the Haskell Platform. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
Hmm, I get Configuring cuda-0.5.0.0... setup.exe: configure script not found. can you help ? Peter I was able to install the cuda package under 32-bit GHC 7.4.2 using the 5.0 SDK and use it from within ghci. This required using my fork of the cuda repo and following the instructions in my WINDOWS.md. Make sure nvcc is in your path (the CUDA installer should have made this so) and try 'cabal configure'. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] install cuda
You need to generate the configure script using autoconf: https://www.gnu.org/software/autoconf/manual/autoconf.html#autoconf-Invocation On 03/31/2013 08:27 PM, Peter Caspers wrote: Hmm, I get Configuring cuda-0.5.0.0... setup.exe: configure script not found. can you help ? Peter I was able to install the cuda package under 32-bit GHC 7.4.2 using the 5.0 SDK and use it from within ghci. This required using my fork of the cuda repo and following the instructions in my WINDOWS.md. Make sure nvcc is in your path (the CUDA installer should have made this so) and try 'cabal configure'. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Organising code in FRP
I am just learning FRP ( via reactive-banana) . so possibly opening a topic already mentionned , apologises in advance, and pointers welcomed. I am wondering about code structuration ? ie spagetti code for the network 1/ in a non trivial FRP applicaiton, how to manage modulatity or structuration of the Network ? ( most of the example I scanned are toy-size). I ca imagine it may not be trvial to find its way around in a large setup ... 2/ what about the separation of layers. I mean fine, we extract the reactive ness from the GUI, and separate the layout of widgets from the behaviors of these great, but is it to then mingle the UI with the business part ( say in banking), and the infrastructure side ( say persistence, comms, transactionnality, etc) in other words, how tdoes the nice abstraction developped ( module/ interface / categoty patterns, monad, etc) coexsit with a netork of FRP event and behaviors ? Any prior art on this ? ( and which place si best to discuss this ?) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] graphical editor links ?
I am designing some graphical editor ( visio - dia like) and would be interested to hear any pointer to help me think on the architecture of this, in term of data structure/ EDSL/ persistence/ paradigm (FP/ FRP/...) for the different layers of abstraction I may see , like rendering libraries ( gtk/wx..)- model of the diagram- semantics ( this is a state diag/ archimate / mind mapping , i.e. what the glyph and lines means ) - persistence Any help pointers welcomed ! ( and which place is best to discuss this ?) Luc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Layout section of Haskell 2010 Language Report -- Notes 12
I'm sure I'm missing something, but I'm having difficulty parsing or
reconciling Note 1 and Note 2 of Section 10.3 (Layout) of the Haskell 2010
Language Report.
http://www.haskell.org/onlinereport/haskell2010/haskellch10.html#x17-17800010.3
Can somebody point me in the right direction?
To be clear, I'm not concerned with GHC behavior or best programming practices
here, only with the specification of the language given in the Report.
Note 1 says, A nested context must be further indented than the enclosing
context ('n' 'm'). If not, 'L' fails, and the compiler should indicate a
layout error.
Note 2 says, If the first token after a 'where' (say) is not indented more
than the enclosing layout context, then the block must be empty, so empty
braces are inserted.
It seems that, in Note 2, the first token necessarily refers to a lexeme
other than '{' (else it would not make sense), in which case a '{n}' token will
have been inserted after 'where' (in the example given in the note), yielding a
nested context which is not indented more than the enclosing layout context,
and thus failing the test in the first sentence of Note 1.
So, in the places where Note 2 would apply, it seems Note 1 would yield a
layout error.
For example, in the following code (replace '.' with space),
f x = let
..g y = 2 * y
..where
..g x
it seems that Note 1 would layout error, yet this seems precisely the case
addressed by Note 2 wherein {} would be inserted after the 'where' yielding
syntactically correct (albeit strange) code.
Any insight would be appreciated.
Thanks,
Seth___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell SBV Package with Z3
Jun Jie: A SymArray is an abstraction of an array that can contain symbolic values, as well as being indexed by a symbolic value. I'm not sure how the example you picked relates. There's a sample program in the SBV distribution that shows how to use SymArray's, maybe looking at that might help: http://hackage.haskell.org/packages/archive/sbv/2.10/doc/html/Data-SBV-Examples-Uninterpreted-AUF.html Feel free to e-mail me privately for further questions on SBV; the mailing list might not be quite appropriate for detailed discussions. -Levent. On Sun, Mar 31, 2013 at 7:12 AM, J. J. W. bsc.j@gmail.com wrote: Dear L. Erkok, First I would like to wish you happy easter and I would like to thank you for your help. I have a couple of more questions. I am now playing with SBV package, however I am not sure if I understand the use of arrays, maybe you can give me some pointers. For example I want to prove the following (note: this example is only used to illustrate my question, I thought I've read somewhere in Haddock that this method only support functions with 7 parameters?) prove $ \(a :: SWord8) b c - a . b b . c == a . c Q.E.D. how should I express this using SymArray? Thanks in advance! Yours sincerely, Jun Jie 2013/3/29 Levent Erkok erk...@gmail.com Sorry, there were a couple of typos in the last example. It should read: allSat $ \(x::SWord8) - x `shiftL` 2 ./= x Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using sat/allSat as opposed to prove, and hence the inversion of equality in the property.) -Levent. On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok erk...@gmail.com wrote: You're welcome Jun Jie. Regarding getting a different counter example: That's perfectly normal. When SMT solvers build models they use random seeds. Furthermore, different versions of the same solver can use different algorithms/heuristics to arrive at the falsifying model. So, it's entirely expected that you get a different counter-example. You can turn the question around, and ask the solver to give you all counter-examples like this: allSat $ \x - \(x::SWord8) - x `shiftL` 2 .!= x -Levent. On Mar 29, 2013, at 1:42 AM, J. J. W. bsc.j@gmail.com wrote: Dear Levent, Thank you for your support. I am very honoured to have the developer of the SBV package to solve my elementary problem. I noticed that the counter-example given by my Z3 differs from the one said on HackageDB: sbv-2.10. Code that is on Hackage: Prelude Data.SBV prove $ forAll [x] $ \(x::SWord8) - x `shiftL` 2 .== x Falsifiable. Counter-example: x = 128 :: SWord8 My current GHCi output: Prelude Data.SBV prove $ forAll [x] $ \(x::SWord8) - x `shiftL` 2 .== x Falsifiable. Counter-example: x = 51 :: SWord8 (0.02 secs, 1196468 bytes) Thank you for your help! Yours sincerely, Jun Jie 2013/3/29 Levent Erkok erk...@gmail.com Hi Jun Jie: SBV uses some of the not-yet-officially-released features in Z3. The version you have, while it's the latest official Z3 release, will not work. To resolve, you need to install the development version of Z3 (something that is at least 4.3.2 or better). Here're instructions from the Microsoft folks explaining how to get these builds: http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html Let me know if you find any issues after you get the latest-development version of Z3 installed. -Levent. On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. bsc.j@gmail.com wrote: Dear all, I have a small question regarding the installation of the SBV package. I first installed the SBV 2.10 package with cabal with the following instructions: cabal install sbv Next I installed the Z3 theorem prover and adding the path to my system variables (Windows 7 x64). Next I tested whether I could find it by opening cmd.exe and then typing z3, I get an error message of Z3, so I can safely assume the system can find it. (I added the path to the bin of Z3, I have not included the include directory, I see no reason why I should add a path to this directory, but maybe I am wrong). I ran the program: SBVUnitTests. However it had some errors in the beginning and afterwards a few failures. Having no idea how to fix this, I continued to check whether I can get the SBV to work. So I started to execute the SBV package: ghci -XScopedTypeVariables ghci :m Data.SBV ghci prove $ \(x::SWord8) - x `shiftL` 2 .== 4*x Now this should return Q.E.D., however it returned the following: An error occured. Failed to complete the call to z3 Executable: C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe Options: /in /smt2 Exit code: 0 Solver output: === ; :smt.mbqi ; :pp.decimal_precision === Giving up.. It does seems
