David BZ told me that the old theory of singular support of $D$-modules fits into the new theory of singular support of coherent sheaves, via the derived loop space.  I wonder how to reconcile that with Gabber's theorem, which gives a strong constraint on what the singular support of a D-module can be, and with my impression that in not-so-derived situations the singular support of a coherent sheaf can be anything.

Here's an attempt to reconstruct it, probably with mistakes, and then a question:

Let $E$ be a complex vector space, and let $LE$ be its derived loop space.  The set of complex points of the once-shifted cotangent bundle of $LE$ can be identified with $E \times E^*$, i.e. the usual cotangent bundle of $E$.  A general construction of Benson-Iyengar-Krause produces a closed subset of $E \times E^*$ from a coherent sheaf on $LE$.  Arinkin and Gaitsgory call it the singular support of the coherent sheaf.

$LE$ has an action of a circle, loop rotation.  Ben-Zvi and Nadler identify the rotation-equivariant coherent sheaves on $LE$ with a category of filtered $D$-modules on $E$.  The associated graded module of the filtered $D$-module is a coherent sheaf on $E \times E^*$, whose support is the singular support or characteristic variety of the $D$-module.  These two notions of singular support match (I heard).

The singular support of a $D$-module is a coisotropic subset of the symplectic $E \times E^*$.  Is that a consequence of any general result about singular support of coherent sheaves?