Bluish Coder

Programming Languages, Martials Arts and Computers. The Weblog of Chris Double.


2010-06-13

Functions in ATS

Using higher order functions in ATS was a bit of a struggle for me at first due to having to deal with getting types correct. I'm coming from a background of dynamically typed languages where it is easy to create and pass around anonymous functions. Even other typed languages like Haskell proved easy to pick up, primarily because of the excellent type inference available. I delved deeper into the different types of functions in ATS to get more familiar with it. This post covers the things that were important for me to start using them successfully in larger ATS programs.

ATS distiguishes between two types of functions:

  • 'functions' which are exactly like functions in C. That is they are a memory address pointing to the machine code for the function body. Functions cannot capture the environment at the point they are created so do not act as 'closures' in other languages. By default top level ATS function definitions are 'functions'. They can be passed directly to external C routines that require function pointers.
  • 'closures' which are functions combined with an environment mapping names to values. These are exactly like closures in other dynamic langauges that enable you to capture variables in the enclosing scope. To create a closure you must explicitly mark it as being a closure. A closure requires memory to be allocated to store the environment. This means you will either need to allocate the closure on the stack (so it is freed automatically when the scope exits), free the memory for the closure manually, or link against the garbage collector.

As well as these two types of functions, ATS can track the effects that occur during a function call. The types of effects that can be tracked are:

  • exn - the function can raise an exception
  • ntm - the function is possibly non-terminating
  • ref - the function may potentially update the content of some shared memory

This leads to a number of combinations that can result in a function having a different type. These effects and whether it is a 'function' or 'closure' are annotated in the function definition as 'tags' in between '<' and '>' before the return type. A function definition without tags looks like:

fun add5 (n: int): int = n+5

Adding tags looks like:

fun add5 (n: int):<tag1,tag2,tag...> int = n+5

The valid values for the tags are:

  • !exn - the function possibly raises exceptions
  • !ntm - the function possibly is non-terminating
  • !ref - the function possibly updates shared memory
  • 0 - the function is pure (has no effects)
  • 1 - the function can have all effects
  • fun - the function is an ordinary, non-closure, function
  • cloptr - the function is a linear closure that must be explicitly freed
  • cloref - the function is a peristent closure that requires the garbage collector to be freed.

Note that the '0' and '1' tags can be suffixed to 'fun', 'cloptr' and 'cloref' for simplicity:

  • fun0 - a pure function
  • fun1 - a function that can have all effects
  • cloptr0 - a linear closure that is pure
  • cloptr1 - a linear closure that can have all effects
  • cloref0 - a persistent closure that is pure
  • cloref1 - a persistent closure that can have all effects

Some examples of tag usage follow. Where more than one usage example is given the definitions are equivalent.

A function that takes an int, returns an int, is pure, doesn't have side effects, doesn't raise exceptions and will terminate:

fun add5 (n: int):<fun0> int = n+5
fun add5 (n: int):<fun> int = n+5
fun add5 (n: int):<> int = n+5

A function that takes an int, returns an int, possibly has side effects, may raise an exception, might not terminate:

fun add5 (n: int):<fun1> int = n+5
fun add5 (n: int):> int = n+5

A function that takes an int, returns an int, is pure except it possibly raises exceptions

fun add5 (n: int):<!exn> int = n+5

An example of usage which causes a compile time error due to effects not matching. The 'outer' function is defined as pure but it is calling an impure function:

fn inner ():<fun1> int = 5
fn outer ():<fun0> int = inner()

implement main() = print_int(inner())

Notice that I use 'fn', not 'fun' here. 'fn' is used to explicitly define a function that cannot be recursive. 'fun' allows a function to call itself and can be recursive. The latter has no termination metrics annotated to the function so you get a compile error if 'fun' is used. I use 'fn' to automatically add the termination metric.

Another compile time error example due to effects not matching is having 'outer' not throw exceptions but calling a function that does:

fn inner ():<!exn> int = 5
fn outer ():<fun0> int = inner()

implement main() = print_int(inner())

The previous example modified so 'outer' can raise exceptions so it will compile:

fn inner ():<!exn> int = 5
fn outer ():<fun0,!exn> int = inner()

implement main() = print_int(inner())

Higher order functions

Functions can take other functions as arguments, or return functions. The types of these functions are defined using a syntax similar to that of defining top level functions except for the following:

  • 'fun' or 'fn' is excluded
  • no function name is given
  • ':' is replaced with '-' before the return value and tags

For example, the following shows ways that function argument and returns types are defined:

typedef foo_t = int -<fun1> int
fun bar (f: foo_t): int = f(42);

fun add5 (n: int): int = n+5
fun baz (): foo_t = add5;

fun bar2 (f: int -<fun1> int) = f(42);
fun baz2 (): int -<fun1> int = add5;

Note that the the effects and types of the functions have to match. Here is an error due to pure vs impure usage:

fun add5 (n: int):<fun1> int = n+5
fun bar (f: int -<fun0> int) = f(42)

implement main() = print_int(bar(add5));

The 'bar' function expects to be passed a pure function as an argument, but 'add5' is impure.

ATS supports creation of anonymous functions using the 'lam' keyword. Anonymous functions using 'lam' are defined similar to the syntax of top level functions except for:

  • 'fun' or 'fun' is replaced with 'lam'
  • no function name is given

For example:

fun bar (f: int -<fun1> int) = f(42)
implement main() = print_int(bar(lam (n) => n+10));

Tags can be used with 'lam' too:

fun bar (f: int -<fun1> int) = f(42)
implement main() = print_int(bar(lam (n) =<fun1> n+10));

Functions of tag 'fun' can be passed directly to C functions that expect 'pointer to function' arguments. For example:

%{^
typedef int (*func)(int);

void adder(func f) {
  int n = f(10);
  printf("from C: %d\n", n);
}
%}

extern fun adder(f: (int) -<fun1> int):<fun1> void = "#adder"
fn add5 (n: int):<fun0> int = n+5
implement main() = adder(add5);

In a followup post I'll go through persistent and linear closures and usage of higher order functions in the ATS library.

Resources that helped with this post:

Tags: ats 

2010-06-02

Safer C Code Using ATS

When developing the original Ogg backend for Firefox we had to integrate and use a number of C libraries. Over the months after landing a number of bugs were raised for various issues in the backend. A fair number of these were the result of common coding errors. Things like not checking return values of the C API calls and not releasing resources correctly. This was internal to the third party libraries we used as well as in our own code. This has made me interested in looking at programming languges that make these sorts of errors easier to find.

I've previously written about ATS, a programming language with dependent and linear types. With ATS you can use C code directly and annotate the code with types to make some usage errors detectable at compile time. Some papers that cover this usage of ATS are:

In this post I look at ways of using a C library from ATS that shows dealing with static checking of return values and resource releasing. I start from a simple wrapper and then explore how I can use ATS to make usage of the API safer from common programmer errors. The library I'm using to do this is libcurl.

A simple usage of libcurl to retrieve the HTML from a URL and print it to stdout is (simple.c):

#include <curl/curl.h>

int main(void)
{
  CURL *curl;
  CURLcode res;

  curl = curl_easy_init();
  curl_easy_setopt(curl, CURLOPT_URL, "bluishcoder.co.nz");
  res = curl_easy_perform(curl);
  curl_easy_cleanup(curl);
  return 0;
}

This can be compiled and run with:

$ gcc -o simple simple.c `curl-config --libs`
$ ./simple
...

Ensuring release of resources

My first attempt at translating this into ATS is in simple1.dats (pretty-printed version):

%{^
#include <curl/curl.h>
%}

absviewtype CURLptr (l:addr) // CURL*

abst@ype CURLoption = $extype "CURLoption"
macdef CURLOPT_URL = $extval(CURLoption, "CURLOPT_URL")

extern fun curl_easy_init
  ()
  : [l:addr] CURLptr l = "#curl_easy_init"
extern fun curl_easy_setopt {l:addr} {p:type}
  (handle: !CURLptr l, option: CURLoption, parameter: p)
  : int = "#curl_easy_setopt"
extern fun curl_easy_perform {l:addr}
  (handle: !CURLptr l)
  : int = "#curl_easy_perform"
extern fun curl_easy_cleanup {l:addr}
  (handle: CURLptr l)
  : void = "#curl_easy_cleanup"

implement main() = let
  val curl  = curl_easy_init();
  val res = curl_easy_setopt(curl, CURLOPT_URL, "www.bluishcoder.co.nz");
  val res = curl_easy_perform(curl);
  val () = curl_easy_cleanup(curl);
in
  ()
end;

The 'main' function looks very much like the C code. The definitions before that make the libcurl C functions, types and enums available to ATS. To compile and run this code:

$ atscc -o simple1 simple1.dats `curl-config --libs`
$ ./simple1
..

The libcurl type CURLoption is a C enum. To wrap this in ATS I use $extype to refer to the C name directly:

abst@ype CURLoption = $extype "CURLoption"

I only reference one value of these types. That is CURLOPT_URL and again I reference the C value directly. Since this is a value rather than a type I use $extval:

macdef CURLOPT_URL = $extval(CURLoption, "CURLOPT_URL")

The CURL type is an abstract type in C - we don't care what it is actually composed of. A CURL object is always refered to via a pointer. This is modeled in ATS with:

absviewtype CURLptr (l:addr) // CURL*

Think of 'CURLptr' as being 'a reference to a CURL object'. It's basically a C 'CURL*'. The definition above states that a CURLptr is an object of type 'CURLptr' located at a memory address 'l'.

The C definition of curl_easy_init looks like:

CURL *curl_easy_init(void);

The ATS definition is:

extern fun curl_easy_init () : [l:addr] CURLptr l = "#curl_easy_init" 

The 'extern' at the beginning and the '#curl_easy_init' at the end means that the implementation of this function is a C function called 'curl_easy_init' in an external library. The '[l:addr]' following the function name gives the type of the 'l' used in the return type - that being a pointer. The return type is 'CURLptr l' which I described previously. The function returns a CURLptr object located at pointer address 'l'.

The C definition of curl_easy_setopt looks like:

CURLcode curl_easy_setopt(CURL *curl, CURLoption option, ...);

It is a C function that takes a variable number of arguments. For this example I'm only using one additional parameter so I cheat and declare it in ATS as accepting one. I'll cover how to do variable argument functions later. The ATS definition is:

extern fun curl_easy_setopt {l:addr} {p:type}
  (handle: !CURLptr l, option: CURLoption, parameter: p)
  : int = "#curl_easy_setopt"

The function takes three arguments and returns one. The arguments it takes are:

  • a '!CURLptr l'. As described before this is a CURLptr object located at address 'l'. The '!' means curl_easy_setopt does not consume the object - we can continue to use it later. The 'l' is declared to be of type 'addr' earlier in the definition using {l:addr}.
  • a 'CURLoption'
  • a parameter value of type 'p'. This is of type 'type' (from the {p:type} earlier in the definition). This is the type of all ATS objects that fit in a machine word (pointers, integers, etc).

The remaining two CURL functions used in the example are variants of these. The main difference is in the ATS definition of 'curl_easy_cleanup':

extern fun curl_easy_cleanup {l:addr}
  (handle: CURLptr l)
  : void = "#curl_easy_cleanup"

Here the 'handle' parameter is a 'CURLptr l'. There is no '!' before it. This means the function consumes the argument and it cannot be used after this call. The type 'CURLptr l' is a linear type. It must be destroyed at some point in the program and once destroyed it cannot be re-used.

By defining 'curl_easy_cleanup' in this way we enforce a contract which states that the programmer must call this function if they have a live 'CURLptr l' object. You can see this in practice if you remove the cleanup call and try to compile. A compile error will result. A compile error will also occur if you try to use the curl handle after the cleanup call.

Because of the usage of the linear type we're already safe from one class of common programmer error. That of not calling cleanup functions for allocated objects.

Handling NULL pointers

There is a bug lurking in this version (and the C program). 'curl_easy_init' can return NULL and if it does you should not call any other curl functions. Using ATS we can define things in such a way that it is a requirement to check for NULL to successfully compile.

A modified version of the example with the changes to support this is in simple2.dats (pretty-printed version).

In this version we expand on the type CURLptr by adding two typedefs. One for pointers which can be NULL (CURLptr0) and one for pointers which cannot be NULL (CURLptr1):

absviewtype CURLptr (l:addr) // CURL*
viewtypedef CURLptr0 = [l:addr | l >= null] CURLptr l
viewtypedef CURLptr1 = [l:addr | l >  null] CURLptr l

The definitions of the Curl functions that are used are changed to use these types in the appropriate places:

extern fun curl_easy_init
  ()
  : CURLptr0 = "#curl_easy_init"
extern fun curl_easy_setopt {p:type}
  (handle: !CURLptr1, option: CURLoption, parameter: p)
  : int = "#curl_easy_setopt"
extern fun curl_easy_perform
  ( handle: !CURLptr1)
  : int = "#curl_easy_perform"
extern fun curl_easy_cleanup
  (handle: CURLptr1)
  : void = "#curl_easy_cleanup"

'curl_easy_init' is changed to return a CURLptr0 since it can return NULL. The other functions use CURLptr1 to signify they must not be NULL. Now if we keep the 'main' function as before without checking the result of 'curl_easy_init' we get a compile time error saying the type of the 'curl' variable does not match that required by 'curl_easy_opt'.

The fix is to add a check for NULL:

implement main() = let
  val curl = curl_easy_init();
  val () = assert_errmsg(CURLptr_isnot_null curl, "curl_easy_init failed");
  val res = curl_easy_setopt(curl, CURLOPT_URL, "www.bluishcoder.co.nz");
  val res = curl_easy_perform(curl);
  val ()  = curl_easy_cleanup(curl);
in
  ()
end;

The compiler knows that after the assert check that 'curl' must not be NULL. This allows the remaining parts of the program to typecheck.

Enforce checking of return values

Another common error is that of not checking the return values of C api calls for errors. This proved to be an issue in the first versions of the Firefox Ogg video backend where return values were not checked in some of the third party libraries we were using. Types can be defined in ATS to give compile time errors if return values are not checked for errors.

'curl_easy_setopt' and 'curl_easy_perform' both return a value indicating success or failure. A non-zero value indicates an error.

See simple3.dats (pretty-printed version) for the changes required to enforce checking of the values. The definition of 'curl_easy_setopt' has changed to:

extern fun curl_easy_setopt {p:type}
  (handle: !CURLptr1 >> opt(CURLptr1, err == 0),
   option: CURLoption, parameter: p)
  : #[err:int] int err = "#curl_easy_setopt"

The same change was made to 'curl_easy_perform'. The parameter 'handle' has changed to have a type of '!CURLptr1 >> opt(CURLptr1, err == 0)'. The type definition before the '>>' is what the function accepts as input. After the '>>' is the type of the parameter after the function returns.

This says that after the function returns the type of 'handle' is a 'CURLptr1' if 'err' is zero. 'err' is defined later in the definition as an integer. This forces calling code to check the return value to see if it is zero. That code can then continue to use the CURLptr1 type by extracting it from the 'opt'. This is the adjusted 'main' function showing how this works:

implement main() = let
  val curl = curl_easy_init();
  val () = assert_errmsg(CURLptr_isnot_null curl, "curl_easy_init failed");
  val res = curl_easy_setopt(curl, CURLOPT_URL, "www.bluishcoder.co.nz");
  val () = assert_errmsg(res = 0, "curl_easy_setopt failed");
  prval () = opt_unsome(curl);
  val res = curl_easy_perform(curl);
  val () = assert_errmsg(res = 0, "curl_easy_perform failed");
  prval () = opt_unsome(curl);
  val ()  = curl_easy_cleanup(curl);
in
 ()
end;

Notice the assertion check for the return value of the functions. This is followed by an 'opt_unsome' call to 'un-opt' the type and continue using it as a 'CURLptr1'. If either the assert check, or the 'opt_unsome' is commented out the code won't compile. If the assert check is done for a value other than zero it won't compile. The code could also check the result using an 'if' statement - I use assert here for brevity.

Tags: ats  mozilla 

2010-05-31

ATS Preforking Echo Server

As an exercise in learning more about ATS I worked on porting the preforking echo server I wrote in Pure. I wanted to get a feel for how higher order functions worked so I followed the same structure as the Pure program.

The code I ended up with is in preforking1.dats. There is also a pretty-printed version produced by 'atsopt'. I posted some questions about my attempt on the ATS mailing list and got a reply clearing some things up and with the example reworked. That reworked example is in preforking2.dats (pretty-printed version)

The Pure code uses 'fdopen' to convert the socket file descriptor to a stdio 'FILE*'. ATS doesn't have fdopen as part of the standard library so I added this with the ability to include inline C code.

The sockets code makes use of ATS features to reduce the chance that sockets are used incorrectly by performing compile time typechecking. The code in 'make_server_socket' looks like this:

fun make_server_socket (port: int) : [fd:int] (socket_v(fd,listen) | int fd) = let
  val (pf_sock_s | sockfd) = socket_family_type_exn (AF_INET, SOCK_STREAM);
  var servaddr: sockaddr_in_struct_t;
  val servport = in_port_nbo_of_int (port);
  val in4addr = in_addr_nbo_of_hbo (INADDR_ANY);
  val () = sockaddr_ipv4_init (servaddr, AF_INET, in4addr, servport);
  val () = bind_ipv4_exn (pf_sock_s | sockfd, servaddr);
  val () = listen_exn (pf_sock_s | sockfd, 10);
in
  (pf_sock_s | sockfd)
end;

The socket functions are defined such that performing operations out of order causes a compile error. Removing the 'listen_exn' line and compiling results in this error (edited for brevity):

preforking1.dats: 2072(line=63, offs=3) -- 2092(line=63, offs=23): 
error(3): mismatch of static terms (tyleq):
  The needed term is: S2Eapp(S2Ecst(socket_v); S2EVar(146), S2Eapp(S2Ecst(listen); ))
  The actual term is: S2Eapp(S2Ecst(socket_v); S2EVar(145), S2Eapp(S2Ecst(bind); ))

This error occurs on the line that returns the result:

(pf_sock_s | sockfd)

The error occurs because the return value of 'make_server_socket' is defined as:

[fd:int] (socket_v(fd,listen) | int fd)

The part of the definition to the left of the pipe character (the '|') is a view that is threaded through calls to the socket functions. The 'listen' part says the socket must be in a state whereby 'listen_exn' was called on it. The function definitions for 'bind_ipv4_exn' and 'listen_exn' are:

fun bind_ipv4_exn {fd:int} (
    pf_sock: !socket_v (fd, init) >> socket_v (fd, bind)
  | fd: int fd, servaddr: &sockaddr_in_struct_t
  ) : void

fun listen_exn {fd:int} (
    pf_sock: !socket_v (fd, bind) >> socket_v (fd, listen)
  | fd: int fd, backlog: Pos
  ) : void

The bind_ipv4_exn definition takes as an argument a socket file descriptor in the 'init' state and leaves it in the 'bind' state. The 'listen_exn' function takes a socket in the 'bind' state and leaves it in the 'listen' state. So by not calling 'listen_exn' we've left the socket in the 'bind' state and that does not match the return value of 'make_server_socket'.

This is all checked at compile time. Everything to the left of the pipe character in a type (the '|') is compile time state and is absent at runtime. So the compiled result of the program knows nothing about the state the socket is in.

For more on this read the ATS tutorial topics on dataviews and dataviewtypes.

Another interesting feature is that the socket code ensures at compile time that the socket has been closed. Removing the following line results in a compile time error:

val () = socket_close_exn(pf_sock_s | sockfd);

The error is:

preforking1.dats: 2118(line=67, offs=21) -- 2861(line=81, offs=4): error(3):
the linear dynamic variable [pf_sock_s] needs to be consumed but it is 
preserved with the type 
[S2Eapp(S2Ecst(socket_v); S2EVar(151), S2Eapp(S2Ecst(listen); ))] instead.

You can see in the definitions of the socket functions whether the pf_sock linear variable is expected to be consumed or not. This is indicated by the exclamation mark (the '!') before the type. Compare the definition of 'listen_exn' with that of 'socket_close_exn':

fun listen_exn {fd:int} (
    pf_sock: !socket_v (fd, bind) >> socket_v (fd, listen)
  | fd: int fd, backlog: Pos
  ) : void

fun socket_close_exn {fd:int} {s:status}
   (pf_sock: socket_v (fd, s) | fd: int fd): void

Notice that 'pf_sock' in 'listen_exn' is '!socket_v' whereas in 'socket_close_exn' it is 'socket_v'. The latter says that the linear variable is consumed and cannot be used after this function is called. It is a compile error to use it after it is consumed. It is also a compile error to not consume the linear variable. I showed the error resulting from not closing the socket, the following is the result of using the socket after closing it:

implement main () = let
  val (pf_sock_s | sockfd) = make_server_socket (5000);
  val () = socket_close_exn(pf_sock_s | sockfd);
  val children = array0_make_arraysize($arrsz{pid_t} (fork_child(pf_sock_s | sockfd, child),
                                                     fork_child(pf_sock_s | sockfd, child)));
  ...

preforking1.dats: 2292(line=70, offs=66) -- 2301(line=70, offs=75): error(3): 
  there is no type for the dynamic variable [pf_sock_s].

As the linear dynamic variable 'pf_sock_s' has been consumed by the 'socket_close_exn' call it is no longer available to the code following it.

The ATS Cairo Tutorial has more examples of using the type system to check errors when calling C code.

The 'child' function has an 'assert_err' call in it to check the result of 'input_line' was a valid line and not an error. It then outputs the line:

val line = input_line(file);
val () = assert_errmsg(stropt_is_some line, #LOCATION);
val () = output_line(file, stropt_unsome(line));

If that assert is removed then a compile error results:

preforking1.dats: 1491(line=48, offs=30) -- 1504(line=48, offs=43): 
error(3): unsolved constraint: 
  C3STRprop(none; S2Eapp(S2Ecst(>=); S2EVar(139), S2Eint(0)))

Not the friendliest error message but the line it points too and the offsets show it as being the 'stropt_unsome(line)' part of the 'output_line' call. The following prelude definitions are relevant here:

fun input_line (fil: FILEref): Stropt
fun output_line (fil: FILEref, line: string): void

castfn stropt_some {n:nat} (str: string n):<> stropt n
castfn stropt_unsome {n:nat} (stropt: stropt n):<> string n
fun stropt_is_none {i:int} (stropt: stropt i):<> bool (i < 0)
fun stropt_is_some {i:int} (stropt: stropt i):<> bool (i >= 0)

'input_line' returns a 'Stropt' but 'output_line' requires a 'string'. 'stropt_unsome' takes a 'stropt' of length 'n' where 'n' is a natural number (positive integer greater than one) and returns a 'string' of the same length.

The result returned from 'input_line' can have a length of zero which doesn't match the type of stropt_unsome which requires a length of one or more. This results in the compile time error when the assertion is removed. The compiler is telling the programmer that they haven't catered for the possible error result of a zero length string returned from 'input_line'.

By adding the assertion there is now a check for the case of the length being zero resultinging in the assertion failure. The compiler now knows that any use of the string after that line must have a length of greater than zero. So the type check to the call of 'stropt_unsome' passes.

The original code I wrote created closures and used some input functions to read from the socket that used heap allocations that results in the garbage collector needing to be linked into the program. In the reworked example posted to the mailing list the code was changed to not require garbage collection to be used. One feature used in that example is allocating closures on the stack instead of the heap. This is done with '@lam':

var !p_clo = @lam
    (pf: !V | pid: &pid_t): void =<clo> let
    val _pid = $effmask_all (waitpid(pid, status, WNONE))
  in
    // nothing
  end 
val () = array_ptr_foreach_clo<pid_t> {V} (view@ status | !p_children, !p_clo, NCHILD)

The 'var !p_clo = @lam' syntax means that the closure is stack allocated and the memory will be reclaimed when the function exits. The 'array_ptr_foreach_clo' call following it then calls this closure on each item in the array of process id's. It's also possible to heap allocate closures and manually free them - linear types ensure the call to free the memory is not forgotten by the programmer. Getting the type annotations for closures is unfortunately tricky and the syntax is a bit painful.

The ATS tutorial has a section on allocation in stack frames and functions vs closures.

Tags: ats 

2010-05-20

Building Firefox with WebM support

All the patches to get Firefox built with WebM support have now been attached to their relevant bugs. These patches aren't ready for review yet but can be used to get a build that has the functionality of the special Firefox WebM builds.

To build use Mozilla Central as the base with the patches from the following bugs applied:

Hopefully these will be finished, reviewed and landed in short order.

Tags: mozilla  firefox  video 

2010-05-20

VP8, WebM and Firefox

For all the details on the recent announcing of VP8 video code support in Firefox, the WebM container and playing YouTube videos with Firefox, read Firefox, YouTube and WebM on hacks.mozilla.org.

More links:

And don't forget the Opera WebM builds and Chromium builds.

To find WebM videos on YouTube:

  1. Search using the YouTube search
  2. On the URL for the search and "&webm=1&html5=1" and visit that URL.
  3. Click on a video.
  4. Add to the end of that video URL: &html5=1
  5. Enjoy WebM goodness.
  6. Right click in Firefox on the video to get fullscreen.

This post is available in the Ukranian language.

Tags: mozilla  firefox  video 


This site is accessable over tor as hidden service 6vp5u25g4izec5c37wv52skvecikld6kysvsivnl6sdg6q7wy25lixad.onion, or Freenet using key:
USK@1ORdIvjL2H1bZblJcP8hu2LjjKtVB-rVzp8mLty~5N4,8hL85otZBbq0geDsSKkBK4sKESL2SrNVecFZz9NxGVQ,AQACAAE/bluishcoder/-61/


Tags

Archives
Links