I'm currently trying to understand the construction of the category of l-adic constructible sheaves as in SGA5, and it seems that quite a lot of machinery (the MLAR condition, localization of the category of projective systems, etc.) has to be gone through before one can even construct this category and show that it's abelian, for instance. On the other hand it is not even true that the derived category of l-adic sheaves is defined in the obvious manner, since it is defined as a 2-limit of the derived categories of $\mathbb{Z}/l^n$ constructible sheaves.

I understand that the categorical machinery in existence today is a lot more powerful than it was in the 1970's, which makes me curious: is there a cleaner and more transparent way of doing this, and a more modern presentation than SGA or Frietag-Kiehl?